Lax Theory Morphisms

DOI10.1145/2818644zbMath1367.03061OpenAlexW2095327196WikidataQ130949019 ScholiaQ130949019MaRDI QIDQ5277906

Florian Rabe

Publication date: 12 July 2017

Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/2818644

zbMATH Keywords

representation theoremtranslationlogical frameworktheory morphismlogical relationdependent type theory

Mathematics Subject Classification ID

Logic in computer science (03B70)

Related Items (1)

The future of logic: foundation-independence

Uses Software

• Isabelle
• OBJ3
• Twelf
• MMT
• QMT
• IMPS
• LATIN

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• A scalable module system
• Representing model theory in a type-theoretical logical framework
• Combinatory logic. With two sections by William Craig.
• IMPS: An interactive mathematical proof system
• Structured theory presentations and logic representations
• Isabelle. A generic theorem prover
• The MMT API: A Generic MKM System
• Proofs for free
• Mechanizing the Metatheory of Sledgehammer
• Logical relations for a logical framework
• How to identify, translate and combine logics?
• A framework for defining logics
• Institutions: abstract model theory for specification and programming
• Project Abstract: Logic Atlas and Integrator (LATIN)
• An Executable Formalization of the HOL/Nuprl Connection in the Metalogical Framework Twelf
• A logical framework combining model and proof theory

This page was built for publication: Lax Theory Morphisms