Lax theory morphisms
From MaRDI portal
Publication:5277906
DOI10.1145/2818644zbMATH Open1367.03061OpenAlexW2095327196WikidataQ130949019 ScholiaQ130949019MaRDI QIDQ5277906FDOQ5277906
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
Recommendations
representation theoremlogical relationtheory morphismtranslationdependent type theorylogical framework
Cites Work
- The MMT API: a generic MKM system
- IMPS: An interactive mathematical proof system
- Isabelle. A generic theorem prover
- How to identify, translate and combine logics?
- A scalable module system
- A framework for defining logics
- Institutions: abstract model theory for specification and programming
- Project abstract: logic atlas and integrator (LATIN)
- Representing model theory in a type-theoretical logical framework
- Combinatory logic. With two sections by William Craig.
- Title not available (Why is that?)
- Proofs for free. Parametricity for dependent types
- Title not available (Why is that?)
- Structured theory presentations and logic representations
- Title not available (Why is that?)
- A logical framework combining model and proof theory
- Mechanizing the metatheory of Sledgehammer
- An Executable Formalization of the HOL/Nuprl Connection in the Metalogical Framework Twelf
- Logical relations for a logical framework
Cited In (5)
Uses Software
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)
