Representing model theory in a type-theoretical logical framework
From MaRDI portal
Publication:654913
Recommendations
- Representing model theory in a type-theoretical logical framework
- Intensional models for the theory of types
- Model-Theoretic Logics
- Abstract deduction and inferential models for type theory
- scientific article; zbMATH DE number 516994
- Equivalences between logics and their representing type theories
- Constructive set theoretic models of typed combinatory logic
- Model theory and the Tannakian formalism
- scientific article; zbMATH DE number 2196607
- scientific article; zbMATH DE number 5316601
Cites work
- scientific article; zbMATH DE number 1617292 (Why is no real title available?)
- scientific article; zbMATH DE number 4130339 (Why is no real title available?)
- scientific article; zbMATH DE number 3148408 (Why is no real title available?)
- scientific article; zbMATH DE number 3819086 (Why is no real title available?)
- scientific article; zbMATH DE number 3695144 (Why is no real title available?)
- scientific article; zbMATH DE number 3754682 (Why is no real title available?)
- scientific article; zbMATH DE number 3521950 (Why is no real title available?)
- scientific article; zbMATH DE number 1216133 (Why is no real title available?)
- scientific article; zbMATH DE number 1078585 (Why is no real title available?)
- scientific article; zbMATH DE number 1086718 (Why is no real title available?)
- scientific article; zbMATH DE number 2003161 (Why is no real title available?)
- scientific article; zbMATH DE number 3997131 (Why is no real title available?)
- scientific article; zbMATH DE number 1863394 (Why is no real title available?)
- scientific article; zbMATH DE number 2196612 (Why is no real title available?)
- scientific article; zbMATH DE number 3280068 (Why is no real title available?)
- scientific article; zbMATH DE number 3331288 (Why is no real title available?)
- A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions
- A framework for defining logics
- Combining Type Theory and Untyped Set Theory
- Consistency of the Continuum Hypothesis. (AM-3)
- Crafting a Proof Assistant
- Encoding modal logics in logical frameworks
- FUNCTORIAL SEMANTICS OF ALGEBRAIC THEORIES
- HOLCF = HOL + LCF
- Institution morphisms
- Institutions: abstract model theory for specification and programming
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Intuitionistic model constructions and normalization proofs
- Isabelle. A generic theorem prover
- Isabelle/HOL. A proof assistant for higher-order logic
- Mizar’s Soft Type System
- Project abstract: logic atlas and integrator (LATIN)
- Proof Systems for Institutional Logic
- Refinement Types as Proof Irrelevance
- Representing model theory in a type-theoretical logical framework
- Some Domain Theory and Denotational Semantics in Coq
- Structural cut elimination. I: Intuitionistic and classical logic
- Structured theory presentations and logic representations
- The calculus of constructions
- Towards a mechanized metatheory of Standard ML
Cited in
(12)- A logical framework combining model and proof theory
- The future of logic: foundation-independence
- Dialectica models of type theory
- A scalable module system
- Model-theoretic conservative extension for definitional theories
- A proof theoretic interpretation of model theoretic hiding
- Towards logical frameworks in the heterogeneous tool set Hets
- Project abstract: logic atlas and integrator (LATIN)
- Lax theory morphisms
- scientific article; zbMATH DE number 516994 (Why is no real title available?)
- Representing model theory in a type-theoretical logical framework
- FoCaLiZe and Dedukti to the rescue for proof interoperability
Describes a project that uses
Uses Software
This page was built for publication: Representing model theory in a type-theoretical logical framework
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q654913)
