The practice of logical frameworks

DOI10.1007/3-540-61064-2_33OpenAlexW1536064546MaRDI QIDQ5878905

Frank Pfenning

Publication date: 23 February 2023

Published in: Trees in Algebra and Programming — CAAP '96 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-61064-2_33

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

A Maude environment for CafeOBJ, Cut-elimination for a logic with definitions and induction

Uses Software

• Coq
• Isabelle/ZF
• Nuprl
• Automath
• LEGO
• Elf

Cites Work

• 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
• Unnamed Item
• Unnamed Item
• Unnamed Item
• On the unity of logic
• Using typed lambda calculus to implement formal systems on a machine
• Partial inductive definitions
• A unification algorithm for typed \(\bar\lambda\)-calculus
• Implementing tactics and tacticals in a higher-order logic programming language
• Experimenting with Isabelle in ZF set theory
• Set theory for verification. I: From foundations to functions
• Structured theory presentations and logic representations
• Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
• The foundation of a generic theorem prover
• Equational reasoning in Isabelle
• Uniform proofs as a foundation for logic programming
• A mechanical proof of the Church-Rosser theorem
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• A framework for defining logics
• Natural deduction as higher-order resolution
• Residual theory in λ-calculus: a formal development
• Linear unification of higher-order patterns
• Higher-order unification with dependent function types
• A termination ordering for higher order rewrite systems
• Problems in rewriting applied to categorical concepts by the example of a computational comonad
• Towards a domain theory for termination proofs
• Higher order conditional rewriting and narrowing
• Representing proof transformations for program optimization
• Tactic theorem proving with refinement-tree proofs and metavariables
• Elf: A meta-language for deductive systems
• A UNIFICATION ALGORITHM FOR THE λΠ-CALCULUS