Representing model theory in a type-theoretical logical framework

DOI10.1016/J.ENTCS.2009.11.005MaRDI QIDQ5170290zbMATH OpenOpenAlexFDO

Authors Fulya Horozal, Florian Rabe

Publication date 23 July 2014

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Copyright license Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International

Full work available at URL https://doi.org/10.1016/j.entcs.2009.11.005

zbMATH Keywords

first-order logiclogical frameworksmodel theory and module systems

Mathematics Subject Classification ID

Classical first-order logic (03B10) Logic in computer science (03B70) Model theory (03C99)

Recommendations

• Representing model theory in a type-theoretical logical framework
• A logical framework combining model and proof theory
• Equivalences between logics and their representing type theories
• Mechanizing metatheory in a logical framework
• scientific article; zbMATH DE number 516994

Cites work

• A framework for defining logics
• Combining Type Theory and Untyped Set Theory
• Encoding modal logics in logical frameworks
• 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 1216133 (Why is no real title available?)
• scientific article; zbMATH DE number 1078585 (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?)
• Institution morphisms
• Institutions: abstract model theory for specification and programming
• Isabelle. A generic theorem prover
• Kripke Semantics for Martin-Löf’s Extensional Type Theory
• Proof Systems for Institutional Logic
• Structural cut elimination. I: Intuitionistic and classical logic
• Structured theory presentations and logic representations

Cited in

(4)

• Model-theoretic conservative extension for definitional theories
• Dialectica models of type theory
• Lax theory morphisms
• Representing model theory in a type-theoretical logical framework

Describes a project that uses

Uses Software

• Isabelle
• Mizar
• Automath
• Nuprl

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 Q5170290)