# nLab Frank Pfenning

Selected writings

## Selected writings

On inductive types and the calculus of constructions:

• Frank Pfenning, Christine Paulin-Mohring, Inductively defined types in the Calculus of Constructions, in: Mathematical Foundations of Programming Semantics MFPS 1989, Lecture Notes in Computer Science 442, Springer (1990) $[$doi:10.1007/BFb0040259$]$

On linear logic and basics of type theory:

• Frank Pfenning, Logical frameworks – a brief introduction (2002) [pdf]

• Frank Pfenning, Logical frameworks, chapter 17 in: Alan Robinson and Andrei Voronkov (eds.): Handbook of Automated Reasoning (1999) 1063-1147 [ps]

• Frank Pfenning, Logical frameworks web site (web), including an extensive bibliography and a list of implementations

On modal logic:

• Frank Pfenning, Rowan Davies, A judgemental reconstruction of modal logic, Mathematical Structures in Comp. Sci. 11 4 (2001) 511-540 [pdf]

• Frank Pfenning, Towards modal type theory (2000) [pdf]

• Frank Pfenning, Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory, in: Symposium on Logic in Computer Science (2001) 221&-230 [web]

On the type of natural numbers in type theory:

category: people

Last revised on January 17, 2023 at 12:36:28. See the history of this page for a list of all contributions to it.