7 Search Results for "Huber, Simon"

Document
DOI: 10.4230/LIPIcs.COSIT.2024.7
What Is a Spatio-Temporal Model Good For?: Validity as a Function of Purpose and the Questions Answered by a Model

Authors: Simon Scheider and Judith A. Verstegen

Published in: LIPIcs, Volume 315, 16th International Conference on Spatial Information Theory (COSIT 2024)

Abstract
The concept of validity is a cornerstone of science. Given this central role, it is somewhat surprising to find that validity remains a rather obscure concept. Unfortunately, the term is often reduced to a matter of ground truth data, seemingly because we fail to come to grips with it. In this paper, instead, we take a purpose-based approach to the validity of spatio-temporal models. We argue that a model application is valid only if the model delivers an answer to a particular spatio-temporal question specifying some experiment including spatio-temporal controls and measures. Such questions constitute the information purposes of models, forming an intermediate layer in a pragmatic knowledge pyramid with corresponding levels of validity. We introduce a corresponding question-based grammar that allows us to formally distinguish among contemporary inference, prediction, retrodiction, projection, and retrojection models. We apply the grammar to corresponding examples and discuss the possibilities for validating such models as a means to a given end.
Cite as

Simon Scheider and Judith A. Verstegen. What Is a Spatio-Temporal Model Good For?: Validity as a Function of Purpose and the Questions Answered by a Model. In 16th International Conference on Spatial Information Theory (COSIT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 315, pp. 7:1-7:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{scheider_et_al:LIPIcs.COSIT.2024.7,
  author =	{Scheider, Simon and Verstegen, Judith A.},
  title =	{{What Is a Spatio-Temporal Model Good For?: Validity as a Function of Purpose and the Questions Answered by a Model}},
  booktitle =	{16th International Conference on Spatial Information Theory (COSIT 2024)},
  pages =	{7:1--7:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-330-0},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{315},
  editor =	{Adams, Benjamin and Griffin, Amy L. and Scheider, Simon and McKenzie, Grant},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.COSIT.2024.7},
  URN =		{urn:nbn:de:0030-drops-208225},
  doi =		{10.4230/LIPIcs.COSIT.2024.7},
  annote =	{Keywords: validity, fitness-for-purpose, spatio-temporal modeling, pragmatics, question grammar}
}
Document
DOI: 10.4230/OASIcs.WCET.2024.2
The Platin Multi-Target Worst-Case Analysis Tool

Authors: Emad Jacob Maroun, Eva Dengler, Christian Dietrich, Stefan Hepp, Henriette Herzog, Benedikt Huber, Jens Knoop, Daniel Wiltsche-Prokesch, Peter Puschner, Phillip Raffeck, Martin Schoeberl, Simon Schuster, and Peter Wägemann

Published in: OASIcs, Volume 121, 22nd International Workshop on Worst-Case Execution Time Analysis (WCET 2024)

Abstract
With the increasing number of applications that require reliable runtime guarantees, the relevance of static worst-case analysis tools that can provide such guarantees increases. These analysis tools determine resource-consumption bounds of application tasks, with a model of the underlying hardware, to meet given resource budgets during runtime, such as deadlines of real-time tasks. This paper presents enhancements to the Platin worst-case analysis tool developed since its original release more than ten years ago. These novelties comprise Platin’s support for new architectures (i.e., ARMv6-M, RISC-V, and AVR) in addition to the previous backends for Patmos and ARMv7-M. Further, Platin now features system-wide analysis methods and annotation support to express system-level constraints. Besides an overview of these enhancements, we evaluate Platin’s accuracy for the two supported architecture implementations, Patmos and RISC-V.
Cite as

Emad Jacob Maroun, Eva Dengler, Christian Dietrich, Stefan Hepp, Henriette Herzog, Benedikt Huber, Jens Knoop, Daniel Wiltsche-Prokesch, Peter Puschner, Phillip Raffeck, Martin Schoeberl, Simon Schuster, and Peter Wägemann. The Platin Multi-Target Worst-Case Analysis Tool. In 22nd International Workshop on Worst-Case Execution Time Analysis (WCET 2024). Open Access Series in Informatics (OASIcs), Volume 121, pp. 2:1-2:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{maroun_et_al:OASIcs.WCET.2024.2,
  author =	{Maroun, Emad Jacob and Dengler, Eva and Dietrich, Christian and Hepp, Stefan and Herzog, Henriette and Huber, Benedikt and Knoop, Jens and Wiltsche-Prokesch, Daniel and Puschner, Peter and Raffeck, Phillip and Schoeberl, Martin and Schuster, Simon and W\"{a}gemann, Peter},
  title =	{{The Platin Multi-Target Worst-Case Analysis Tool}},
  booktitle =	{22nd International Workshop on Worst-Case Execution Time Analysis (WCET 2024)},
  pages =	{2:1--2:14},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-346-1},
  ISSN =	{2190-6807},
  year =	{2024},
  volume =	{121},
  editor =	{Carle, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2024.2},
  URN =		{urn:nbn:de:0030-drops-204704},
  doi =		{10.4230/OASIcs.WCET.2024.2},
  annote =	{Keywords: worst-case resource consumption, WCET, static analysis tool}
}
Document
DOI: 10.4230/OASIcs.WCET.2019.4
Worst-Case Energy-Consumption Analysis by Microarchitecture-Aware Timing Analysis for Device-Driven Cyber-Physical Systems

Authors: Phillip Raffeck, Christian Eichler, Peter Wägemann, and Wolfgang Schröder-Preikschat

Published in: OASIcs, Volume 72, 19th International Workshop on Worst-Case Execution Time Analysis (WCET 2019)

Abstract
Many energy-constrained cyber-physical systems require both timeliness and the execution of tasks within given energy budgets. That is, besides knowledge on worst-case execution time (WCET), the worst-case energy consumption (WCEC) of operations is essential. Unfortunately, WCET analysis approaches are not directly applicable for deriving WCEC bounds in device-driven cyber-physical systems: For example, a single memory operation can lead to a significant power-consumption increase when thereby switching on a device (e.g. transceiver, actuator) in the embedded system. However, as we demonstrate in this paper, existing approaches from microarchitecture-aware timing analysis (i.e. considering cache and pipeline effects) are beneficial for determining WCEC bounds: We extended our framework on whole-system analysis with microarchitecture-aware timing modeling to precisely account for the execution time that devices are kept (in)active. Our evaluations based on a benchmark generator, which is able to output benchmarks with known baselines (i.e. actual WCET and actual WCEC), and an ARM Cortex-M4 platform validate that the approach significantly reduces analysis pessimism in whole-system WCEC analyses.
Cite as

Phillip Raffeck, Christian Eichler, Peter Wägemann, and Wolfgang Schröder-Preikschat. Worst-Case Energy-Consumption Analysis by Microarchitecture-Aware Timing Analysis for Device-Driven Cyber-Physical Systems. In 19th International Workshop on Worst-Case Execution Time Analysis (WCET 2019). Open Access Series in Informatics (OASIcs), Volume 72, pp. 4:1-4:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{raffeck_et_al:OASIcs.WCET.2019.4,
  author =	{Raffeck, Phillip and Eichler, Christian and W\"{a}gemann, Peter and Schr\"{o}der-Preikschat, Wolfgang},
  title =	{{Worst-Case Energy-Consumption Analysis by Microarchitecture-Aware Timing Analysis for Device-Driven Cyber-Physical Systems}},
  booktitle =	{19th International Workshop on Worst-Case Execution Time Analysis (WCET 2019)},
  pages =	{4:1--4:12},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-118-4},
  ISSN =	{2190-6807},
  year =	{2019},
  volume =	{72},
  editor =	{Altmeyer, Sebastian},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2019.4},
  URN =		{urn:nbn:de:0030-drops-107699},
  doi =		{10.4230/OASIcs.WCET.2019.4},
  annote =	{Keywords: WCEC, WCRE, WCET, michroarchitecture analysis, whole-system analysis}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2019.11
Homotopy Canonicity for Cubical Type Theory

Authors: Thierry Coquand, Simon Huber, and Christian Sattler

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)

Abstract
Cubical type theory provides a constructive justification of homotopy type theory and satisfies canonicity: every natural number is convertible to a numeral. A crucial ingredient of cubical type theory is a path lifting operation which is explained computationally by induction on the type involving several non-canonical choices. In this paper we show by a sconing argument that if we remove these equations for the path lifting operation from the system, we still retain homotopy canonicity: every natural number is path equal to a numeral.
Cite as

Thierry Coquand, Simon Huber, and Christian Sattler. Homotopy Canonicity for Cubical Type Theory. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 11:1-11:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{coquand_et_al:LIPIcs.FSCD.2019.11,
  author =	{Coquand, Thierry and Huber, Simon and Sattler, Christian},
  title =	{{Homotopy Canonicity for Cubical Type Theory}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{11:1--11:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Geuvers, Herman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.11},
  URN =		{urn:nbn:de:0030-drops-105188},
  doi =		{10.4230/LIPIcs.FSCD.2019.11},
  annote =	{Keywords: cubical type theory, univalence, canonicity, sconing, Artin glueing}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2019.25
Gluing for Type Theory

Authors: Ambrus Kaposi, Simon Huber, and Christian Sattler

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)

Abstract
The relationship between categorical gluing and proofs using the logical relation technique is folklore. In this paper we work out this relationship for Martin-Löf type theory and show that parametricity and canonicity arise as special cases of gluing. The input of gluing is two models of type theory and a pseudomorphism between them and the output is a displayed model over the first model. A pseudomorphism preserves the categorical structure strictly, the empty context and context extension up to isomorphism, and there are no conditions on preservation of type formers. We look at three examples of pseudomorphisms: the identity on the syntax, the interpretation into the set model and the global section functor. Gluing along these result in syntactic parametricity, semantic parametricity and canonicity, respectively.
Cite as

Ambrus Kaposi, Simon Huber, and Christian Sattler. Gluing for Type Theory. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 25:1-25:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{kaposi_et_al:LIPIcs.FSCD.2019.25,
  author =	{Kaposi, Ambrus and Huber, Simon and Sattler, Christian},
  title =	{{Gluing for Type Theory}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{25:1--25:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Geuvers, Herman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.25},
  URN =		{urn:nbn:de:0030-drops-105323},
  doi =		{10.4230/LIPIcs.FSCD.2019.25},
  annote =	{Keywords: Martin-L\"{o}f type theory, logical relations, parametricity, canonicity, quotient inductive types}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2015.5
Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom

Authors: Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg

Published in: LIPIcs, Volume 69, 21st International Conference on Types for Proofs and Programs (TYPES 2015) (2018)

Abstract
This paper presents a type theory in which it is possible to directly manipulate $n$-dimensional cubes (points, lines, squares, cubes, etc.) based on an interpretation of dependent type theory in a cubical set model. This enables new ways to reason about identity types, for instance, function extensionality is directly provable in the system. Further, Voevodsky's univalence axiom is provable in this system. We also explain an extension with some higher inductive types like the circle and propositional truncation. Finally we provide semantics for this cubical type theory in a constructive meta-theory.
Cite as

Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 5:1-5:34, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{cohen_et_al:LIPIcs.TYPES.2015.5,
  author =	{Cohen, Cyril and Coquand, Thierry and Huber, Simon and M\"{o}rtberg, Anders},
  title =	{{Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom}},
  booktitle =	{21st International Conference on Types for Proofs and Programs (TYPES 2015)},
  pages =	{5:1--5:34},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-030-9},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{69},
  editor =	{Uustalu, Tarmo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015.5},
  URN =		{urn:nbn:de:0030-drops-84754},
  doi =		{10.4230/LIPIcs.TYPES.2015.5},
  annote =	{Keywords: univalence axiom, dependent type theory, cubical sets}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2013.107
A Model of Type Theory in Cubical Sets

Authors: Marc Bezem, Thierry Coquand, and Simon Huber

Published in: LIPIcs, Volume 26, 19th International Conference on Types for Proofs and Programs (TYPES 2013)

Abstract
We present a model of type theory with dependent product, sum, and identity, in cubical sets. We describe a universe and explain how to transform an equivalence between two types into an equality. We also explain how to model propositional truncation and the circle. While not expressed internally in type theory, the model is expressed in a constructive metalogic. Thus it is a step towards a computational interpretation of Voevodsky's Univalence Axiom.
Cite as

Marc Bezem, Thierry Coquand, and Simon Huber. A Model of Type Theory in Cubical Sets. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 107-128, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{bezem_et_al:LIPIcs.TYPES.2013.107,
  author =	{Bezem, Marc and Coquand, Thierry and Huber, Simon},
  title =	{{A Model of Type Theory in Cubical Sets}},
  booktitle =	{19th International Conference on Types for Proofs and Programs (TYPES 2013)},
  pages =	{107--128},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-72-9},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{26},
  editor =	{Matthes, Ralph and Schubert, Aleksy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.107},
  URN =		{urn:nbn:de:0030-drops-46284},
  doi =		{10.4230/LIPIcs.TYPES.2013.107},
  annote =	{Keywords: Models of dependent type theory, cubical sets, Univalent Foundations}
}
  • Refine by Author
  • 4 Huber, Simon
  • 3 Coquand, Thierry
  • 2 Raffeck, Phillip
  • 2 Sattler, Christian
  • 2 Wägemann, Peter
  • Show More...

  • Refine by Classification

  • Refine by Keyword
  • 2 WCET
  • 2 canonicity
  • 2 cubical sets
  • 1 Artin glueing
  • 1 Martin-Löf type theory
  • Show More...

  • Refine by Type
  • 7 document

  • Refine by Publication Year
  • 3 2019
  • 2 2024
  • 1 2014
  • 1 2018

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 About DROPS Imprint Privacy Contact