License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2020.24
URN: urn:nbn:de:0030-drops-123466
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/12346/
Go to the corresponding LIPIcs Volume Portal

Diezel, Tim Lukas ; Goncharov, Sergey

Towards Constructive Hybrid Semantics

pdf-format:
LIPIcs-FSCD-2020-24.pdf (0.6 MB)

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.

BibTeX - Entry

@InProceedings{diezel_et_al:LIPIcs:2020:12346,
  author =	{Tim Lukas Diezel and Sergey Goncharov},
  title =	{{Towards Constructive Hybrid Semantics}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{24:1--24:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Zena M. Ariola},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/12346},
  URN =		{urn:nbn:de:0030-drops-123466},
  doi =		{10.4230/LIPIcs.FSCD.2020.24},
  annote =	{Keywords: Hybrid semantics, Elgot iteration, Homotopy type theory, Agda}
}

Keywords: Hybrid semantics, Elgot iteration, Homotopy type theory, Agda
Collection: 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)
Issue Date: 2020
Date of publication: 28.06.2020
Supplementary Material: The recent version of our implementation can be found at https://github.com/sergey-goncharov/hybrid-agda.

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI