A logical framework combining model and proof theory

DOI10.1017/S0960129512000424zbMath1326.03082OpenAlexW2003075592MaRDI QIDQ5400853

Florian Rabe

Publication date: 12 March 2014

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0960129512000424

zbMATH Keywords

institutionsEdinburgh logical framework LFmachine-verified encodings of logics

Mathematics Subject Classification ID

Related Items (8)

Lax Theory Morphisms ⋮ Presentation and manipulation of Mizar properties in an Isabelle object logic ⋮ A Proof Theoretic Interpretation of Model Theoretic Hiding ⋮ Towards Logical Frameworks in the Heterogeneous Tool Set Hets ⋮ A scalable module system ⋮ Graded consequence: an institution theoretic study ⋮ Project Abstract: Logic Atlas and Integrator (LATIN) ⋮ Semantics of Mizar as an Isabelle object logic

Uses Software

• Coq
• Isabelle
• LEO-II
• Isabelle/HOL
• CASL
• PVS
• Mizar
• ETPS
• HOL Light
• Twelf
• Automath
• Agda
• Delphin

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• Representing model theory in a type-theoretical logical framework
• Using typed lambda calculus to implement formal systems on a machine
• Grothendieck institutions
• Institution morphisms
• Generalized algebraic theories and contextual categories
• The calculus of constructions
• Structured theory presentations and logic representations
• May I borrow your logic? (Transporting logical structures along maps)
• A linear logical framework
• Encoding modal logics in logical frameworks
• Structural cut elimination. I: Intuitionistic and classical logic
• Stratified institutions and elementary homomorphisms
• Institution-independent model theory
• Intuitionistic model constructions and normalization proofs
• Towards Logical Frameworks in the Heterogeneous Tool Set Hets
• Formalising foundations of mathematics
• Some Domain Theory and Denotational Semantics in Coq
• Locally cartesian closed categories and type theory
• Proof Systems for Institutional Logic
• Towards MKM in the Large: Modular Representation and Scalable Software Architecture
• An Interpretation of Isabelle/HOL in HOL Light
• A framework for defining logics
• Adjointness in Foundations
• Institutions: abstract model theory for specification and programming
• Weak inclusion systems
• MathScheme: Project Description
• Importing HOL Light into Coq
• A Mechanized Translation from Higher-Order Logic to Set Theory
• Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
• A formulation of the simple theory of types
• Completeness in the theory of types

This page was built for publication: A logical framework combining model and proof theory