Lax theory morphisms

DOI10.1145/2818644MaRDI QIDQ5277906zbMATH OpenOpenAlexWikidataFDO

Authors 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 theoremlogical relationtheory morphismtranslationdependent type theorylogical framework

Mathematics Subject Classification ID

Logic in computer science (03B70)

Recommendations

• scientific article; zbMATH DE number 1670816
• scientific article; zbMATH DE number 2003150
• Institution morphisms
• Representing model theory in a type-theoretical logical framework
• L ax F: Side Conditions and External Evidence as Monads

Cites work

• scientific article; zbMATH DE number 1670816 (Why is no real title available?)
• scientific article; zbMATH DE number 3819086 (Why is no real title available?)
• scientific article; zbMATH DE number 3467028 (Why is no real title available?)
• A framework for defining logics
• A logical framework combining model and proof theory
• A scalable module system
• An Executable Formalization of the HOL/Nuprl Connection in the Metalogical Framework Twelf
• Combinatory logic. With two sections by William Craig.
• How to identify, translate and combine logics?
• IMPS: An interactive mathematical proof system
• Institutions: abstract model theory for specification and programming
• Isabelle. A generic theorem prover
• Logical relations for a logical framework
• Mechanizing the metatheory of Sledgehammer
• Project abstract: logic atlas and integrator (LATIN)
• Proofs for free. Parametricity for dependent types
• Representing model theory in a type-theoretical logical framework
• Structured theory presentations and logic representations
• The MMT API: a generic MKM system

Cited in

(5)

• The future of logic: foundation-independence
• Lax Monoidal Fibrations
• Lax Functors, Cospans, and the Center Construction
• scientific article; zbMATH DE number 4095730 (Why is no real title available?)
• scientific article; zbMATH DE number 2003150 (Why is no real title available?)

Describes a project that uses

Uses Software

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

This page was built for publication: Lax theory morphisms

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5277906)