Skip to Main content Skip to Navigation
Conference papers

Structuring Theories with Implicit Morphisms

Abstract : We introduce implicit morphisms as a concept in formal systems based on theories and theory morphisms. The idea is that there may be at most one implicit morphism from a theory S to a theory T, and if S-expressions are used in T their semantics is obtained by automatically inserting the implicit morphism. The practical appeal of implicit morphisms is that they hit the sweet-spot of being extremely simple to understand and implement while significantly helping with structuring large collections of theories.Concrete applications include elegantly identifying isomorphic theories and extending theories with definitions and theorems as well as efficiently building and maintaining large, fine-granular, and heterogeneous hierarchies of theories. Our results are formulated and implemented in the language and system, and we expect they can be transferred to other morphism-based formalisms relatively easily.
Document type :
Conference papers
Complete list of metadata

Cited literature [7 references]  Display  Hide  Download

https://hal.inria.fr/hal-02364570
Contributor : Hal Ifip <>
Submitted on : Friday, November 15, 2019 - 9:03:02 AM
Last modification on : Friday, April 30, 2021 - 10:01:51 AM
Long-term archiving on: : Sunday, February 16, 2020 - 1:52:40 PM

File

 Restricted access
To satisfy the distribution rights of the publisher, the document is embargoed until : 2022-01-01

Please log in to resquest access to the document

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Florian Rabe, Dennis Müller. Structuring Theories with Implicit Morphisms. 24th International Workshop on Algebraic Development Techniques (WADT), Jul 2018, Egham, United Kingdom. pp.154-173, ⟨10.1007/978-3-030-23220-7_9⟩. ⟨hal-02364570⟩

Share

Metrics

Record views

81