Representing model theory in a type-theoretical logical framework
From MaRDI portal
Publication:654913
DOI10.1016/j.tcs.2011.03.022zbMath1236.03027OpenAlexW2046048646MaRDI QIDQ654913
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
first-order logiclogical frameworkproof-theoretic semanticsmodel-theoretic semanticsTwelf module system
Logic in computer science (03B70) Classical first-order logic (03B10) Applications of model theory (03C98)
Related Items
Lax Theory Morphisms, A Proof Theoretic Interpretation of Model Theoretic Hiding, Towards Logical Frameworks in the Heterogeneous Tool Set Hets, A scalable module system, FoCaLiZe and Dedukti to the rescue for proof interoperability, A logical framework combining model and proof theory, Project Abstract: Logic Atlas and Integrator (LATIN), The future of logic: foundation-independence
Uses Software
Cites Work
- Institution morphisms
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- The calculus of constructions
- Structured theory presentations and logic representations
- Isabelle. A generic theorem prover
- Encoding modal logics in logical frameworks
- Isabelle/HOL. A proof assistant for higher-order logic
- A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions
- Structural cut elimination. I: Intuitionistic and classical logic
- Intuitionistic model constructions and normalization proofs
- Some Domain Theory and Denotational Semantics in Coq
- Towards a mechanized metatheory of standard ML
- Proof Systems for Institutional Logic
- Mizar’s Soft Type System
- Crafting a Proof Assistant
- Combining Type Theory and Untyped Set Theory
- Refinement Types as Proof Irrelevance
- A framework for defining logics
- HOLCF = HOL + LCF
- Institutions: abstract model theory for specification and programming
- Representing Model Theory in a Type-Theoretical Logical Framework
- Project Abstract: Logic Atlas and Integrator (LATIN)
- FUNCTORIAL SEMANTICS OF ALGEBRAIC THEORIES
- Consistency of the Continuum Hypothesis. (AM-3)
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
