Representing model theory in a type-theoretical logical framework
DOI10.1016/J.TCS.2011.03.022zbMATH Open1236.03027OpenAlexW2046048646MaRDI QIDQ654913FDOQ654913
Authors: Fulya Horozal, Florian Rabe 
Publication date: 23 December 2011
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.tcs.2011.03.022
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
first-order logicproof-theoretic semanticslogical frameworkmodel-theoretic semanticsTwelf module system
Classical first-order logic (03B10) Logic in computer science (03B70) Applications of model theory (03C98)
Cites Work
- Title not available (Why is that?)
- Isabelle. A generic theorem prover
- Isabelle/HOL. A proof assistant for higher-order logic
- Crafting a Proof Assistant
- A framework for defining logics
- Title not available (Why is that?)
- Institutions: abstract model theory for specification and programming
- Title not available (Why is that?)
- Project abstract: logic atlas and integrator (LATIN)
- FUNCTORIAL SEMANTICS OF ALGEBRAIC THEORIES
- Title not available (Why is that?)
- Consistency of the Continuum Hypothesis. (AM-3)
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Institution morphisms
- The calculus of constructions
- Structured theory presentations and logic representations
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Towards a mechanized metatheory of Standard ML
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions
- Encoding modal logics in logical frameworks
- Structural cut elimination. I: Intuitionistic and classical logic
- Intuitionistic model constructions and normalization proofs
- Some Domain Theory and Denotational Semantics in Coq
- Proof Systems for Institutional Logic
- Mizar’s Soft Type System
- Combining Type Theory and Untyped Set Theory
- Refinement Types as Proof Irrelevance
- Title not available (Why is that?)
- HOLCF = HOL + LCF
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Representing model theory in a type-theoretical logical framework
Cited In (12)
- A logical framework combining model and proof theory
- Dialectica models of type theory
- The future of logic: foundation-independence
- 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
- Title not available (Why is that?)
- Representing model theory in a type-theoretical logical framework
- FoCaLiZe and Dedukti to the rescue for proof interoperability
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)
