Frank Pfenning
Department of Computer Science
Carnegie Mellon University

"A Judgmental Reconstruction of Modal Logics"

ABSTRACT

Traditional formulations of modal logic do not separate judgments from
propositions.  As Martin-Lof has pointed out, conflating these notions can
lead to difficulties and the resulting systems often have undesirable
properties.  In this talk we introduce the judgments of necessary and possible
truth of a proposition and develop a corresponding calculus of natural
deduction.  We relate this briefly to traditional formulations of
intuitionistic modal logic and lax logic.  We then sketch computational
interpretations, which include run-time code generation, Moggi's computational
lambda-calculus as analyzed by Kobayashi, and intensional manipulation of
functional expressions.

REFERENCE

Frank Pfenning and Rowan Davies.
A Judgmental Reconstruction of Modal Logic,
Mathematical Structures in Computer Science, to appear.

Paper for an invited talk at the Workshop on Intuitionistic Modal Logics and
Applications, Trento, Italy, July 1999.

Draft available as http://www.cs.cmu.edu/~fp/papers/modal99.ps.gz

Back to Talks Page