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