nLab Frank Pfenning

Selected writings

Selected writings

On higher-order abstract syntax:

On inductive types and the calculus of constructions:

On Semi-axiomatic sequent calculus?:

  • Henry DeYoung?, Frank Pfenning, and Klaas Pruiksma?. Semi-axiomatic sequent calculus. In Z. Ariola, editor, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), pages 29:1–29:22, Paris, France, June 2020. LIPIcs 167. [bib | .pdf]

On linear logic and basics of type theory:

On logical frameworks:

  • 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 modal type theory:

On the type of natural numbers in type theory:

On adjoint logic:

category: people

Last revised on February 7, 2024 at 14:12:28. See the history of this page for a list of all contributions to it.