Using typed lambda calculus to implement formal systems on a machine

DOI10.1007/BF00245294zbMath0784.68072OpenAlexW2010273585MaRDI QIDQ688571

Arnon Avron, Robert Pollack, Ian A. Mason, Furio Honsell

Publication date: 20 December 1993

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf00245294

zbMATH Keywords

formal systemslambda calculusEdinburgh logical frameworkproof checking

Mathematics Subject Classification ID

Logic in computer science (03B70) Combinatory logic and lambda calculus (03B40)

Related Items

LF+ in Coq for "fast and loose" reasoning ⋮ Structured theory presentations and logic representations ⋮ A note on the proof theory of the \(\lambda \Pi\)-calculus ⋮ The semantics and proof theory of linear logic ⋮ Structuring metatheory on inductive definitions ⋮ Logic representation in LF ⋮ A first order logic of effects ⋮ Twenty years of rewriting logic ⋮ The expressive power of Structural Operational Semantics with explicit assumptions ⋮ Mechanizing type environments in weak HOAS ⋮ Equivalences between logics and their representing type theories ⋮ Forum: A multiple-conclusion specification logic ⋮ A logical framework combining model and proof theory ⋮ A natural deduction approach to dynamic logic ⋮ Applicable Mathematics in a Minimal Computational Theory of Sets ⋮ Using typed lambda calculus to implement formal systems on a machine ⋮ Theo: An interactive proof development system ⋮ A type-theoretic approach to program development ⋮ Subtyping dependent types ⋮ The foundation of a generic theorem prover ⋮ A practical implementation of simple consequence relations using inductive definitions ⋮ Developing (Meta)Theory of λ-calculus in the Theory of Contexts1 1Work partially supported by Italian MURST project tosca and EC-WG types. ⋮ Comparing Higher-Order Encodings in Logical Frameworks and Tile Logic ⋮ Proof-search in type-theoretic languages: An introduction ⋮ \(\pi\)-calculus in (Co)inductive-type theory ⋮ Term-generic logic ⋮ Structuring metatheory on inductive definitions ⋮ On the formalization of the modal \(\mu\)-calculus in the calculus of inductive constructions ⋮ A Framework for Defining Logical Frameworks ⋮ Introduction: Non-classical Logics—Between Semantics and Proof Theory (In Relation to Arnon Avron’s Work) ⋮ The practice of logical frameworks

Uses Software

• Nuprl
• Automath
• LEGO
• Elf

Cites Work

• Modal logics for communicating systems
• Linear logic
• Using typed lambda calculus to implement formal systems on a machine
• A logic covering undefinedness in program proofs
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Simple consequence relations
• The semantics and proof theory of linear logic
• The calculus of constructions
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• The foundation of a generic theorem prover
• What is an inference rule?
• A framework for defining logics
• Natural deduction as higher-order resolution
• A formulation of the simple theory of types
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item