Logical frameworks

MaRDI QIDQ2751369zbMATH OpenFDO

Authors Frank Pfenning

Publication date 27 August 2002

zbMATH Keywords

natural deductionproof searchmeta-programmingabstract syntaxlogical frameworkjudgmentshereditary Harrop formulasLF type theoryspecification of deductive systems

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35) Logic in computer science (03B70)

Recommendations

• scientific article; zbMATH DE number 2110615
• scientific article; zbMATH DE number 65531
• Using typed lambda calculus to implement formal systems on a machine
• Functional and Logic Programming
• A meta linear logical framework

Cited in

(33)

• Automated techniques for provably safe mobile code.
• The future of logic: foundation-independence
• A practical implementation of simple consequence relations using inductive definitions
• Functional and Logic Programming
• Directly reflective meta-programming
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
• The Twelf Proof Assistant
• Formal logic definitions for interchange languages
• Efficient substitution in Hoare logic expressions
• A complete uniform substitution calculus for differential dynamic logic
• A framework for defining logical frameworks
• Flexary operators for formalized mathematics
• scientific article; zbMATH DE number 65532 (Why is no real title available?)
• scientific article; zbMATH DE number 4033057 (Why is no real title available?)
• A linear logical framework
• Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics
• Types for Proofs and Programs
• Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge
• On the formalization of the modal -calculus in the calculus of inductive constructions
• Reaping the benefits of modularization in flexiformal mathematics by GF-based AST transformations
• Decidability of bounded higher-order unification
• Cut elimination for a logic with induction and co-induction
• Finitary type theories with and without contexts
• Formalizing adequacy: a case study for higher-order abstract syntax
• Encoding abstract syntax without fresh names
• A logical framework perspective on conservativity
• A third-order representation of the -calculus
• Logical Mappings
• scientific article; zbMATH DE number 4092734 (Why is no real title available?)
• A meta linear logical framework
• scientific article; zbMATH DE number 2110615 (Why is no real title available?)
• Imperative LF meta-programming
• Normalization for the simply-typed lambda-calculus in Twelf

Describes a project that uses

Uses Software

• Elf
• Isabelle

This page was built for publication: Logical frameworks

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