View Full Document

6 views

Unformatted text preview:

Electronic Notes in Computer Science 1 1995 On a Modal Calculus for S4 F Pfenning Department of Computer Science Carnegie Mellon University Pittsburgh PA 15213 U S A fp cs cmu edu H C Wong Department of Computer Science Carnegie Mellon University Pittsburgh PA 15213 U S A hcwong cs cmu edu Abstract We present 2 a concise formulation of a proof term calculus for the intuitionistic modal logic S4 that is well suited for practical applications We show that with respect to provability it is equivalent to other formulations in the literature sketch a simple type checking algorithm and prove subject reduction and the existence of canonical forms for well typed terms Applications include a new formulation of natural deduction for intuitionistic linear logic modal logical frameworks and a logical analysis of staged computation and binding time analysis for functional languages 6 1 Introduction Modal operators familiar from traditional logic have received renewed attention in computer science through their importance in linear logic Typically they are described axiomatically in the style of Hilbert or via sequent calculi However the Curry Howard isomorphism between proofs and terms is most poignant for natural deduction so natural deduction formulations of modal and linear logics have also been the subject of research 20 1 5 3 4 22 13 This work is supported by NSF Grant CCR 9303383 and the Advanced Research Projects Agency under ARPA Order No 8313 c 1995 Elsevier Publishers B V and the author F Pfenning and H C Wong Although most of the researchers in this area agree on the potential applications of modal logics the works published to date seem to be primarily oriented toward proof theory and not well suited for practical applications Among the application areas of modal and linear logics are those of functional programming and logical frameworks In these settings the simplicity of the language a feasible type checking procedure the existence of canonical forms and the



Access the best Study Guides, Lecture Notes and Practice Exams

Loading Unlocking...
Login

Join to view Notes and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Notes and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?