Towards constructive hybrid semantics
Diezel TL, Goncharov S (2020)
Publication Type: Conference contribution, Original article
Publication year: 2020
Journal
Publisher: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Book Volume: 167
Conference Proceedings Title: Leibniz International Proceedings in Informatics, LIPIcs
Event location: Virtual, Online, FRA
ISBN: 9783959771559
DOI: 10.4230/LIPIcs.FSCD.2020.24
Abstract
With hybrid systems becoming ever more pervasive, the underlying semantic challenges emerge in their entirety. The need for principled semantic foundations has been recognized previously in the case of discrete computation and discrete data, with subsequent implementations in programming languages and proof assistants. Hybrid systems, contrastingly, do not directly fit into the classical semantic paradigms due to the presence of quite specific “non-programmable” features, such as Zeno behaviour and the inherent indispensable reliance on a notion of continuous time. Here, we analyze the phenomenon of hybrid semantics from a constructive viewpoint. In doing so, we propose a monad-based semantics, generic over a given ordered monoid representing the time domain, hence abstracting from the monoid of constructive reals. We implement our construction as a higher inductive-inductive type in the recent cubical extension of the Agda proof assistant, significantly using state-of-the-art advances of homotopy type theory. We show that classically, i.e. under the axiom of choice, our construction admits a charaterization in terms of directed sequence completion.
Authors with CRIS profile
How to cite
APA:
Diezel, T.L., & Goncharov, S. (2020). Towards constructive hybrid semantics. In Zena M. Ariola (Eds.), Leibniz International Proceedings in Informatics, LIPIcs. Virtual, Online, FRA, FR: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing.
MLA:
Diezel, Tim Lukas, and Sergey Goncharov. "Towards constructive hybrid semantics." Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020, Virtual, Online, FRA Ed. Zena M. Ariola, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2020.
BibTeX: Download