Using typed lambda calculus to implement formal systems on a machine

DOI10.1007/BF00245294zbMATH Open0784.68072OpenAlexW2010273585MaRDI QIDQ688571FDOQ688571

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

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

Recommendations

• scientific article; zbMATH DE number 4061194
• A tutorial implementation of a dependently typed lambda calculus
• Some lambda calculus and type theory formalized
• A typed, algebraic, computational lambda-calculus
• scientific article; zbMATH DE number 4058907
• Realizing the dependently typed \(\lambda\)-calculus
• Publication:4490735
• scientific article; zbMATH DE number 1499090
• An implementation model of the typed \(\lambda\)-calculus based on linear chemical abstract machine
• Membrane Computing

zbMATH Keywords

lambda calculusformal systemsEdinburgh logical frameworkproof checking

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (38)

• A logical framework combining model and proof theory
• Structuring metatheory on inductive definitions
• Twenty years of rewriting logic
• A type-theoretic approach to program development
• Theo: An interactive proof development system
• A practical implementation of simple consequence relations using inductive definitions
• The foundation of a generic theorem prover
• A first order logic of effects
• The semantics and proof theory of linear logic
• A framework for defining logical frameworks
• A natural deduction approach to dynamic logic
• Forum: A multiple-conclusion specification logic
• TinkerType: a language for playing with formal systems
• Subtyping dependent types
• Comparing higher-order encodings in logical frameworks and tile logic
• Introduction: Non-classical Logics—Between Semantics and Proof Theory (In Relation to Arnon Avron’s Work)
• Developing (meta)theory of \(\lambda\)-calculus in the theory of contexts
• Title not available (Why is that?)
• LF+ in Coq for "fast and loose" reasoning
• \(\pi\)-calculus in (Co)inductive-type theory
• Realizing the dependently typed \(\lambda\)-calculus
• Mechanizing type environments in weak HOAS
• Title not available (Why is that?)
• On the formalization of the modal \(\mu\)-calculus in the calculus of inductive constructions
• The expressive power of Structural Operational Semantics with explicit assumptions
• Logical frameworks
• Equivalences between logics and their representing type theories
• A note on the proof theory of the \(\lambda \Pi\)-calculus
• Structuring metatheory on inductive definitions
• Investigations into proof-search in a system of first-order dependent function types
• Structured theory presentations and logic representations
• Applicable mathematics in a minimal computational theory of sets
• Proof-search in type-theoretic languages: An introduction
• Term-generic logic
• Using typed lambda calculus to implement formal systems on a machine
• Embedding display calculi into logical frameworks: Comparing Twelf and Isabelle
• The practice of logical frameworks
• Logic representation in LF

Uses Software

• Nuprl
• Automath
• LEGO
• Elf

This page was built for publication: Using typed lambda calculus to implement formal systems on a machine

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