A Framework for Defining Logical Frameworks

DOI10.1016/j.entcs.2007.02.014zbMath1277.03029OpenAlexW2123020468MaRDI QIDQ2864157

Luigi Liquori, Furio Honsell, Marina Lenisa

Publication date: 6 December 2013

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2007.02.014

zbMATH Keywords

pattern matchinglambda calculuslogical frameworkdependent-type systems

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

LF+ in Coq for "fast and loose" reasoning, Mechanizing common knowledge logic using COQ, Lambda calculus with patterns, Plugging-in proof development environments usingLocksinLF

Uses Software

• Nuprl
• Twelf
• Automath
• Cambridge LCF

Cites Work

• Using typed lambda calculus to implement formal systems on a machine
• Lambda calculus with patterns
• The calculus of constructions
• Adding algebraic rewriting to the untyped lambda calculus
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• On \(\Pi\)-conversion in the \(\lambda\)-cube and the combination with abbreviations
• Combinatory reduction systems: Introduction and survey
• Theorem proving modulo
• Encoding modal logics in logical frameworks
• \(\pi\)-calculus in (Co)inductive-type theory
• Pure patterns type systems
• A framework for defining logics
• Types for Proofs and Programs
• Programming Languages and Systems
• Parallel reductions in \(\lambda\)-calculus
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item