A logical framework combining model and proof theory (Q5400853): Difference between revisions

@@ Property / describes a project that uses @@
+Isabelle
@@ Property / describes a project that uses: Isabelle / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle/HOL
@@ Property / describes a project that uses: Isabelle/HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Mizar
@@ Property / describes a project that uses: Mizar / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+ETPS
@@ Property / describes a project that uses: ETPS / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Agda
@@ Property / describes a project that uses: Agda / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+LEO-II
@@ Property / describes a project that uses: LEO-II / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+CASL
@@ Property / describes a project that uses: CASL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Automath
@@ Property / describes a project that uses: Automath / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / cites work @@
+A linear logical framework
@@ Property / cites work: A linear logical framework / rank @@
+Normal rank
@@ Property / cites work @@
+Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
+Normal rank
@@ Property / cites work @@
+May I borrow your logic? (Transporting logical structures along maps)
+Normal rank
@@ Property / cites work @@
+Weak inclusion systems
@@ Property / cites work: Weak inclusion systems / rank @@
+Normal rank
@@ Property / cites work @@
+Q3727946
@@ Property / cites work: Q3727946 / rank @@
+Normal rank
@@ Property / cites work @@
+A Mechanized Translation from Higher-Order Logic to Set Theory
+Normal rank
@@ Property / cites work @@
+Towards MKM in the Large: Modular Representation and Scalable Software Architecture
+Normal rank
@@ Property / cites work @@
+Importing HOL Light into Coq
@@ Property / cites work: Importing HOL Light into Coq / rank @@
+Normal rank
@@ Property / cites work @@
+Formalising foundations of mathematics
@@ Property / cites work: Formalising foundations of mathematics / rank @@
+Normal rank
@@ Property / cites work @@
+Representing model theory in a type-theoretical logical framework
+Normal rank
@@ Property / cites work @@
+Completeness in the theory of types
@@ Property / cites work: Completeness in the theory of types / rank @@
+Normal rank
@@ Property / cites work @@
+Structured theory presentations and logic representations
+Normal rank
@@ Property / cites work @@
+Stratified institutions and elementary homomorphisms
+Normal rank
@@ Property / cites work @@
+Locally cartesian closed categories and type theory
+Normal rank
@@ Property / cites work @@
+The calculus of constructions
@@ Property / cites work: The calculus of constructions / rank @@
+Normal rank
@@ Property / cites work @@
+Intuitionistic model constructions and normalization proofs
+Normal rank
@@ Property / cites work @@
+Towards Logical Frameworks in the Heterogeneous Tool Set Hets
+Normal rank
@@ Property / cites work @@
+MathScheme: Project Description
@@ Property / cites work: MathScheme: Project Description / rank @@
+Normal rank
@@ Property / cites work @@
+A formulation of the simple theory of types
@@ Property / cites work: A formulation of the simple theory of types / rank @@
+Normal rank
@@ Property / cites work @@
+A framework for defining logics
@@ Property / cites work: A framework for defining logics / rank @@
+Normal rank
@@ Property / cites work @@
+Q3943975
@@ Property / cites work: Q3943975 / rank @@
+Normal rank
@@ Property / cites work @@
+Institution morphisms
@@ Property / cites work: Institution morphisms / rank @@
+Normal rank
@@ Property / cites work @@
+Institutions: abstract model theory for specification and programming
+Normal rank
@@ Property / cites work @@
+Linear logic
@@ Property / cites work: Linear logic / rank @@
+Normal rank
@@ Property / cites work @@
+Institution-independent model theory
@@ Property / cites work: Institution-independent model theory / rank @@
+Normal rank
@@ Property / cites work @@
+Proof Systems for Institutional Logic
@@ Property / cites work: Proof Systems for Institutional Logic / rank @@
+Normal rank
@@ Property / cites work @@
+Grothendieck institutions
@@ Property / cites work: Grothendieck institutions / rank @@
+Normal rank
@@ Property / cites work @@
+Generalized algebraic theories and contextual categories
+Normal rank
@@ Property / cites work @@
+Structural cut elimination. I: Intuitionistic and classical logic
+Normal rank
@@ Property / cites work @@
+Q4663946
@@ Property / cites work: Q4663946 / rank @@
+Normal rank
@@ Property / cites work @@
+An Interpretation of Isabelle/HOL in HOL Light
@@ Property / cites work: An Interpretation of Isabelle/HOL in HOL Light / rank @@
+Normal rank
@@ Property / cites work @@
+Q4215784
@@ Property / cites work: Q4215784 / rank @@
+Normal rank
@@ Property / cites work @@
+Adjointness in Foundations
@@ Property / cites work: Adjointness in Foundations / rank @@
+Normal rank
@@ Property / cites work @@
+Some Domain Theory and Denotational Semantics in Coq
+Normal rank
@@ Property / cites work @@
+Q4406531
@@ Property / cites work: Q4406531 / rank @@
+Normal rank
@@ Property / cites work @@
+Encoding modal logics in logical frameworks
@@ Property / cites work: Encoding modal logics in logical frameworks / rank @@
+Normal rank
@@ Property / cites work @@
+Using typed lambda calculus to implement formal systems on a machine
+Normal rank
@@ Property / cites work @@
+Q4726218
@@ Property / cites work: Q4726218 / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1017/s0960129512000424
+Normal rank
@@ Property / OpenAlex ID @@
+W2003075592
@@ Property / OpenAlex ID: W2003075592 / rank @@
+Normal rank