1 Search Results for "Diezel, Tim Lukas"

Document
DOI: 10.4230/LIPIcs.FSCD.2020.24
Towards Constructive Hybrid Semantics

Authors: Tim Lukas Diezel and Sergey Goncharov

Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)

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.
Cite as

Tim Lukas Diezel and Sergey Goncharov. Towards Constructive Hybrid Semantics. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 24:1-24:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{diezel_et_al:LIPIcs.FSCD.2020.24,
  author =	{Diezel, Tim Lukas and Goncharov, Sergey},
  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 =	{Ariola, Zena M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.24},
  URN =		{urn:nbn:de:0030-drops-123466},
  doi =		{10.4230/LIPIcs.FSCD.2020.24},
  annote =	{Keywords: Hybrid semantics, Elgot iteration, Homotopy type theory, Agda}
}
  • Refine by Author
  • 1 Diezel, Tim Lukas
  • 1 Goncharov, Sergey

  • Refine by Classification
  • 1 Theory of computation → Axiomatic semantics
  • 1 Theory of computation → Categorical semantics

  • Refine by Keyword
  • 1 Agda
  • 1 Elgot iteration
  • 1 Homotopy type theory
  • 1 Hybrid semantics

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2020

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact