Logical frameworks

MaRDI QIDQ2751369zbMATH OpenFDO

Authors Frank Pfenning

Publication date 27 August 2002

zbMATH Keywords

abstract syntaxhereditary Harrop formulasjudgmentsLF type theorylogical frameworkmeta-programmingnatural deductionproof searchspecification of deductive systems

Mathematics Subject Classification ID

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

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

(37)

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

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)