A framework for defining logical frameworks

DOI10.1016/J.ENTCS.2007.02.014MaRDI QIDQ2864157zbMATH OpenOpenAlexFDO

Authors Furio Honsell, Marina Lenisa, Luigi Liquori

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

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

Recommendations

• A Conditional Logical Framework
• An open logical framework
• scientific article; zbMATH DE number 2110615
• A framework for defining logics
• scientific article; zbMATH DE number 65531

Cites work

• scientific article; zbMATH DE number 1722700 (Why is no real title available?)
• scientific article; zbMATH DE number 4014675 (Why is no real title available?)
• scientific article; zbMATH DE number 4191621 (Why is no real title available?)
• scientific article; zbMATH DE number 3910392 (Why is no real title available?)
• scientific article; zbMATH DE number 3735770 (Why is no real title available?)
• scientific article; zbMATH DE number 2061705 (Why is no real title available?)
• scientific article; zbMATH DE number 1759486 (Why is no real title available?)
• scientific article; zbMATH DE number 4116521 (Why is no real title available?)
• A framework for defining logics
• Adding algebraic rewriting to the untyped lambda calculus
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Combinatory reduction systems: Introduction and survey
• Encoding modal logics in logical frameworks
• Lambda calculus with patterns
• Logical frameworks
• On -conversion in the -cube and the combination with abbreviations
• Parallel reductions in \(\lambda\)-calculus
• Programming Languages and Systems
• Proof-assistants using dependent type systems
• Pure patterns type systems
• The calculus of constructions
• Theorem proving modulo
• Types for Proofs and Programs
• Using typed lambda calculus to implement formal systems on a machine
• -calculus in (Co)inductive-type theory

Cited in

(13)

• Plugging-in proof development environments using \textit{locks} in \(\mathsf{LF}\)
• Lambda calculus with patterns
• Easy definition of new facets in the frame-based language Objlog+
• An open logical framework
• Reflective metalogical frameworks
• Mechanizing common knowledge logic using COQ
• PAL⁺: a lambda-free logical framework
• LF+ in Coq for "fast and loose" reasoning
• A Conditional Logical Framework
• scientific article; zbMATH DE number 1292298 (Why is no real title available?)
• A logical framework with explicit conversions
• Gluing together proof environments: canonical extensions of LF type theories featuring locks
• A definitional implementation of the Lax logical framework \(\mathsf{LLF}_{\mathscr{P}}\) in \texttt{Coq}, for supporting fast and loose reasoning

Describes a project that uses

Uses Software

• Cambridge LCF
• Automath
• Twelf
• Nuprl

This page was built for publication: A framework for defining logical frameworks

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2864157)