Disjunctive Tautologies as Synchronisation Schemes

In the ambient logic of classical second order propositional calculus, we solve the specification problem for a family of excluded middle like tautologies. These are shown to be realized by sequential simulations of specific communication schemes for which they provide a safe typing mechanism.

• Type: Conference
• Year: 2000
• Where: CSL
• Authors: Vincent Danos, Jean-Louis Krivine
• Keywords: Automated Reasoning, CSL 2000, Order Propositional Calculus, Safe Typing Mechanism, Specific Communication Schemes