Representing Model Theory in a Type-Theoretical Logical Framework

DOI10.1016/j.entcs.2009.11.005zbMath1291.03068OpenAlexW1982273589MaRDI QIDQ5170290

Fulya Horozal, Florian Rabe

Publication date: 23 July 2014

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

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

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

Related Items (1)

Representing model theory in a type-theoretical logical framework

Uses Software

• Isabelle
• Mizar
• Nuprl
• Automath

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Institution morphisms
• Structured theory presentations and logic representations
• Isabelle. A generic theorem prover
• Encoding modal logics in logical frameworks
• Structural cut elimination. I: Intuitionistic and classical logic
• Proof Systems for Institutional Logic
• Combining Type Theory and Untyped Set Theory
• Kripke Semantics for Martin-Löf’s Extensional Type Theory
• A framework for defining logics
• Institutions: abstract model theory for specification and programming

This page was built for publication: Representing Model Theory in a Type-Theoretical Logical Framework