4 Search Results for "Hammond, Kevin"


Document
Blame Tracking and Type Error Debugging

Authors: Sheng Chen and John Peter Campora III

Published in: LIPIcs, Volume 136, 3rd Summit on Advances in Programming Languages (SNAPL 2019)


Abstract
In this work, we present an unexpected connection between gradual typing and type error debugging. Namely, we illustrate that gradual typing provides a natural way to defer type errors in statically ill-typed programs, providing more feedback than traditional approaches to deferring type errors. When evaluating expressions that lead to runtime type errors, the usefulness of the feedback depends on blame tracking, the defacto approach to locating the cause of such runtime type errors. Unfortunately, blame tracking suffers from the bias problem for type error localization in languages with type inference. We illustrate and formalize the bias problem for blame tracking, present ideas for adapting existing type error debugging techniques to combat this bias, and outline further challenges.

Cite as

Sheng Chen and John Peter Campora III. Blame Tracking and Type Error Debugging. In 3rd Summit on Advances in Programming Languages (SNAPL 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 136, pp. 2:1-2:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{chen_et_al:LIPIcs.SNAPL.2019.2,
  author =	{Chen, Sheng and Campora III, John Peter},
  title =	{{Blame Tracking and Type Error Debugging}},
  booktitle =	{3rd Summit on Advances in Programming Languages (SNAPL 2019)},
  pages =	{2:1--2:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-113-9},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{136},
  editor =	{Lerner, Benjamin S. and Bod{\'\i}k, Rastislav and Krishnamurthi, Shriram},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2019.2},
  URN =		{urn:nbn:de:0030-drops-105451},
  doi =		{10.4230/LIPIcs.SNAPL.2019.2},
  annote =	{Keywords: Blame tracking, type error debugging, gradual typing, type inference}
}
Document
Terminal Semantics for Codata Types in Intensional Martin-Löf Type Theory

Authors: Benedikt Ahrens and Régis Spadotti

Published in: LIPIcs, Volume 39, 20th International Conference on Types for Proofs and Programs (TYPES 2014)


Abstract
We study the notions of relative comonad and comodule over a relative comonad. We use these notions to give categorical semantics for the coinductive type families of streams and of infinite triangular matrices and their respective cosubstitution operations in intensional Martin-Löf type theory. Our results are mechanized in the proof assistant Coq.

Cite as

Benedikt Ahrens and Régis Spadotti. Terminal Semantics for Codata Types in Intensional Martin-Löf Type Theory. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 1-26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{ahrens_et_al:LIPIcs.TYPES.2014.1,
  author =	{Ahrens, Benedikt and Spadotti, R\'{e}gis},
  title =	{{Terminal Semantics for Codata Types in Intensional Martin-L\"{o}f Type Theory}},
  booktitle =	{20th International Conference on Types for Proofs and Programs (TYPES 2014)},
  pages =	{1--26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-88-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{39},
  editor =	{Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.1},
  URN =		{urn:nbn:de:0030-drops-54891},
  doi =		{10.4230/LIPIcs.TYPES.2014.1},
  annote =	{Keywords: relative comonad, Martin-L\"{o}f type theory, coinductive type, computer theorem proving}
}
Document
Automatic Amortised Worst-Case Execution Time Analysis

Authors: Christoph A. Herrmann, Armelle Bonenfant, Kevin Hammond, Steffen Jost, Hans-Wolfgang Loidl, and Robert Pointon

Published in: OASIcs, Volume 6, 7th International Workshop on Worst-Case Execution Time Analysis (WCET'07) (2007)


Abstract
Our research focuses on formally bounded WCET analysis, where we aim to provide absolute guarantees on execution time bounds. In this paper, we describe how amortisation can be used to improve the quality of the results that are obtained from a fully-automatic and formally guaranteed WCET analysis, by delivering analysis results that are parameterised on specific input patterns and which take account of relations between these patterns. We have implemented our approach to give a tool that is capable of predicting execution costs for a typical embedded system development platform, a Renesas board with a Renesas M32C/85U processor. We show that not only is the amortised approach applicable in theory, but that it can be applied automatically to yield good WCET results.

Cite as

Christoph A. Herrmann, Armelle Bonenfant, Kevin Hammond, Steffen Jost, Hans-Wolfgang Loidl, and Robert Pointon. Automatic Amortised Worst-Case Execution Time Analysis. In 7th International Workshop on Worst-Case Execution Time Analysis (WCET'07). Open Access Series in Informatics (OASIcs), Volume 6, pp. 1-6, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2007)


Copy BibTex To Clipboard

@InProceedings{herrmann_et_al:OASIcs.WCET.2007.1186,
  author =	{Herrmann, Christoph A. and Bonenfant, Armelle and Hammond, Kevin and Jost, Steffen and Loidl, Hans-Wolfgang and Pointon, Robert},
  title =	{{Automatic Amortised Worst-Case Execution Time Analysis}},
  booktitle =	{7th International Workshop on Worst-Case Execution Time Analysis (WCET'07)},
  pages =	{1--6},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-05-7},
  ISSN =	{2190-6807},
  year =	{2007},
  volume =	{6},
  editor =	{Rochange, Christine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2007.1186},
  URN =		{urn:nbn:de:0030-drops-11868},
  doi =		{10.4230/OASIcs.WCET.2007.1186},
  annote =	{Keywords: Amortisation, functional programming, performance measurement, static analysis, type and effect systems, worst-case execution time}
}
Document
Towards Formally Verifiable WCET Analysis for a Functional Programming Language

Authors: Kevin Hammond, Christian Ferdinand, Reinhold Heckmann, Roy Dyckhoff, Martin Hofman, Steffen Jost, Hans-Wolfgang Loidl, Greg Michaelson, Robert Pointon, Norman Scaife, Jocelyn Sérot, and Andy Wallace

Published in: OASIcs, Volume 4, 6th International Workshop on Worst-Case Execution Time Analysis (WCET'06) (2006)


Abstract
This paper describes ongoing work aimed at the construction of formal cost models and analyses to yield verifiable guarantees of resource usage in the context of real-time embedded systems. Our work is conducted in terms of the domain-specific language Hume, a language that combines functional programming for computations with finitestate automata for specifying reactive systems. We outline an approach in which high-level information derived from source-code analysis can be combined with worst-case execution time information obtained from high quality abstract interpretation of low-level binary code.

Cite as

Kevin Hammond, Christian Ferdinand, Reinhold Heckmann, Roy Dyckhoff, Martin Hofman, Steffen Jost, Hans-Wolfgang Loidl, Greg Michaelson, Robert Pointon, Norman Scaife, Jocelyn Sérot, and Andy Wallace. Towards Formally Verifiable WCET Analysis for a Functional Programming Language. In 6th International Workshop on Worst-Case Execution Time Analysis (WCET'06). Open Access Series in Informatics (OASIcs), Volume 4, pp. 1-6, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2006)


Copy BibTex To Clipboard

@InProceedings{hammond_et_al:OASIcs.WCET.2006.677,
  author =	{Hammond, Kevin and Ferdinand, Christian and Heckmann, Reinhold and Dyckhoff, Roy and Hofman, Martin and Jost, Steffen and Loidl, Hans-Wolfgang and Michaelson, Greg and Pointon, Robert and Scaife, Norman and S\'{e}rot, Jocelyn and Wallace, Andy},
  title =	{{Towards Formally Verifiable WCET Analysis for a Functional Programming Language}},
  booktitle =	{6th International Workshop on Worst-Case Execution Time Analysis (WCET'06)},
  pages =	{1--6},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-03-3},
  ISSN =	{2190-6807},
  year =	{2006},
  volume =	{4},
  editor =	{Mueller, Frank},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2006.677},
  URN =		{urn:nbn:de:0030-drops-6773},
  doi =		{10.4230/OASIcs.WCET.2006.677},
  annote =	{Keywords: Worst-case execution time, functional programming, Hume, cost model, asynchronous, finite state machine}
}
  • Refine by Author
  • 2 Hammond, Kevin
  • 2 Jost, Steffen
  • 2 Loidl, Hans-Wolfgang
  • 2 Pointon, Robert
  • 1 Ahrens, Benedikt
  • Show More...

  • Refine by Classification
  • 1 Theory of computation → Type structures

  • Refine by Keyword
  • 2 functional programming
  • 1 Amortisation
  • 1 Blame tracking
  • 1 Hume
  • 1 Martin-Löf type theory
  • Show More...

  • Refine by Type
  • 4 document

  • Refine by Publication Year
  • 1 2006
  • 1 2007
  • 1 2015
  • 1 2019

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