A logical framework combining model and proof theory
From MaRDI portal
Recommendations
Cites work
- scientific article; zbMATH DE number 3959364 (Why is no real title available?)
- scientific article; zbMATH DE number 3761372 (Why is no real title available?)
- scientific article; zbMATH DE number 1216133 (Why is no real title available?)
- scientific article; zbMATH DE number 1936671 (Why is no real title available?)
- scientific article; zbMATH DE number 2152345 (Why is no real title available?)
- scientific article; zbMATH DE number 3999882 (Why is no real title available?)
- A formulation of the simple theory of types
- A framework for defining logics
- A linear logical framework
- A mechanized translation from higher-order logic to set theory
- Adjointness in Foundations
- An Interpretation of Isabelle/HOL in HOL Light
- Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
- Completeness in the theory of types
- Encoding modal logics in logical frameworks
- Formalising foundations of mathematics
- Generalized algebraic theories and contextual categories
- Grothendieck institutions
- Importing HOL Light into Coq
- Institution morphisms
- Institution-independent model theory
- Institutions: abstract model theory for specification and programming
- Intuitionistic model constructions and normalization proofs
- Linear logic
- Locally cartesian closed categories and type theory
- MathScheme: project description
- May I borrow your logic? (Transporting logical structures along maps)
- Proof Systems for Institutional Logic
- Representing model theory in a type-theoretical logical framework
- Some Domain Theory and Denotational Semantics in Coq
- Stratified institutions and elementary homomorphisms
- Structural cut elimination. I: Intuitionistic and classical logic
- Structured theory presentations and logic representations
- The calculus of constructions
- Towards MKM in the large: modular representation and scalable software architecture
- Towards logical frameworks in the heterogeneous tool set Hets
- Using typed lambda calculus to implement formal systems on a machine
- Weak inclusion systems
Cited in
(16)- Semantics of Mizar as an Isabelle object logic
- Project abstract: logic atlas and integrator (LATIN)
- Frontiers of Combining Systems
- scientific article; zbMATH DE number 1418814 (Why is no real title available?)
- A model-theoretic approach to proof theory. Edited by Zofia Adamowicz, Teresa Bigorajska and Konrad Zdanowski
- A proof theoretic interpretation of model theoretic hiding
- Towards logical frameworks in the heterogeneous tool set Hets
- Graded consequence: an institution theoretic study
- How to identify, translate and combine logics?
- Presentation and manipulation of Mizar properties in an Isabelle object logic
- Lax theory morphisms
- The future of logic: foundation-independence
- A scalable module system
- Representing model theory in a type-theoretical logical framework
- A proof-irrelevant model of Martin-Löf's logical framework
- Equivalences among various logical frameworks of partial algebras
Describes a project that uses
Uses Software
This page was built for publication: A logical framework combining model and proof theory
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5400853)
