Representing model theory in a type-theoretical logical framework (Q654913): Difference between revisions

@@ Property / cites work @@
+Crafting a Proof Assistant
@@ Property / cites work: Crafting a Proof Assistant / rank @@
+Normal rank
@@ Property / cites work @@
+Q3937387
@@ Property / cites work: Q3937387 / 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 @@
+Q2722016
@@ Property / cites work: Q2722016 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3889024
@@ Property / cites work: Q3889024 / rank @@
+Normal rank
@@ Property / cites work @@
+Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
+Normal rank
@@ Property / cites work @@
+Some Domain Theory and Denotational Semantics in Coq
+Normal rank
@@ Property / cites work @@
+Combining Type Theory and Untyped Set Theory
@@ Property / cites work: Combining Type Theory and Untyped Set Theory / rank @@
+Normal rank
@@ Property / cites work @@
+Intuitionistic model constructions and normalization proofs
+Normal rank
@@ Property / cites work @@
+Q5565113
@@ Property / cites work: Q5565113 / rank @@
+Normal rank
@@ Property / cites work @@
+The calculus of constructions
@@ Property / cites work: The calculus of constructions / rank @@
+Normal rank
@@ Property / cites work @@
+A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions
+Normal rank
@@ Property / cites work @@
+Q5610115
@@ Property / cites work: Q5610115 / 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 @@
+Q4723263
@@ Property / cites work: Q4723263 / rank @@
+Normal rank
@@ Property / cites work @@
+Institutions: abstract model theory for specification and programming
+Normal rank
@@ Property / cites work @@
+Consistency of the Continuum Hypothesis. (AM-3)
@@ Property / cites work: Consistency of the Continuum Hypothesis. (AM-3) / rank @@
+Normal rank
@@ Property / cites work @@
+Institution morphisms
@@ Property / cites work: Institution morphisms / 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 @@
+Representing Model Theory in a Type-Theoretical Logical Framework
+Normal rank
@@ Property / cites work @@
+Structured theory presentations and logic representations
+Normal rank
@@ Property / cites work @@
+Project Abstract: Logic Atlas and Integrator (LATIN)
+Normal rank
@@ Property / cites work @@
+Q4215784
@@ Property / cites work: Q4215784 / rank @@
+Normal rank
@@ Property / cites work @@
+FUNCTORIAL SEMANTICS OF ALGEBRAIC THEORIES
@@ Property / cites work: FUNCTORIAL SEMANTICS OF ALGEBRAIC THEORIES / rank @@
+Normal rank
@@ Property / cites work @@
+Towards a mechanized metatheory of standard ML
@@ Property / cites work: Towards a mechanized metatheory of standard ML / rank @@
+Normal rank
@@ Property / cites work @@
+Refinement Types as Proof Irrelevance
@@ Property / cites work: Refinement Types as Proof Irrelevance / rank @@
+Normal rank
@@ Property / cites work @@
+Q3032225
@@ Property / cites work: Q3032225 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5311059
@@ Property / cites work: Q5311059 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4099613
@@ Property / cites work: Q4099613 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4360856
@@ Property / cites work: Q4360856 / rank @@
+Normal rank
@@ Property / cites work @@
+HOLCF = HOL + LCF
@@ Property / cites work: HOLCF = HOL + LCF / rank @@
+Normal rank
@@ Property / cites work @@
+Q4362967
@@ Property / cites work: Q4362967 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4435474
@@ Property / cites work: Q4435474 / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+Q4790669
@@ Property / cites work: Q4790669 / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle. A generic theorem prover
@@ Property / cites work: Isabelle. A generic theorem prover / rank @@
+Normal rank
@@ Property / cites work @@
+Structural cut elimination. I: Intuitionistic and classical logic
+Normal rank
@@ Property / cites work @@
+Q3666260
@@ Property / cites work: Q3666260 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3265664
@@ Property / cites work: Q3265664 / rank @@
+Normal rank
@@ Property / cites work @@
+Mizar’s Soft Type System
@@ Property / cites work: Mizar’s Soft Type System / rank @@
+Normal rank