2 Search Results for "Chrzaszcz, Jacek"

Document
DOI: 10.4230/LIPIcs.TYPES.2016.8
Coq Support in HAHA

Authors: Jacek Chrzaszcz, Aleksy Schubert, and Jakub Zakrzewski

Published in: LIPIcs, Volume 97, 22nd International Conference on Types for Proofs and Programs (TYPES 2016)

Abstract
HAHA is a tool that helps in teaching and learning Hoare logic. It is targeted at an introductory course on software verification. We present a set of new features of the HAHA verification environment that exploit Coq. These features are (1) generation of verification conditions in Coq so that they can be explored and proved interactively and (2) compilation of HAHA programs into CompCert certified compilation tool-chain. With the interactive Coq proving support we obtain an interesting functionality that makes it possible to carefully examine step-by-step verification conditions and systematically discover flaws in their formulation. As a result Coq back-end serves as a kind of specification debugger.
Cite as

Jacek Chrzaszcz, Aleksy Schubert, and Jakub Zakrzewski. Coq Support in HAHA. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 8:1-8:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{chrzaszcz_et_al:LIPIcs.TYPES.2016.8,
  author =	{Chrzaszcz, Jacek and Schubert, Aleksy and Zakrzewski, Jakub},
  title =	{{Coq Support in HAHA}},
  booktitle =	{22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
  pages =	{8:1--8:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-065-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{97},
  editor =	{Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.8},
  URN =		{urn:nbn:de:0030-drops-98562},
  doi =		{10.4230/LIPIcs.TYPES.2016.8},
  annote =	{Keywords: Hoare logic, program verification, Coq theorem prover, teaching}
}
Document
DOI: 10.4230/LIPIcs.CSL.2012.198
ML with PTIME complexity guarantees

Authors: Jacek Chrzaszcz and Aleksy Schubert

Published in: LIPIcs, Volume 16, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (2012)

Abstract
Implicit Computational Complexity is a line of research where the possibility to inference a valid property for a program implies that the program runs in particular complexity class. Soft type systems are one of the research threads within the field. We present here a soft type system with ML-like polymorphism that enjoys decidable typechecking, type inference and typability problems and gives polynomial time computational guarantees for the running time of typed programs.
Cite as

Jacek Chrzaszcz and Aleksy Schubert. ML with PTIME complexity guarantees. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 198-212, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{chrzaszcz_et_al:LIPIcs.CSL.2012.198,
  author =	{Chrzaszcz, Jacek and Schubert, Aleksy},
  title =	{{ML with PTIME complexity guarantees}},
  booktitle =	{Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
  pages =	{198--212},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-42-2},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{16},
  editor =	{C\'{e}gielski, Patrick and Durand, Arnaud},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.198},
  URN =		{urn:nbn:de:0030-drops-36738},
  doi =		{10.4230/LIPIcs.CSL.2012.198},
  annote =	{Keywords: implicit computational complexity, polymorphism, soft type assignment}
}
  • Refine by Author
  • 2 Chrzaszcz, Jacek
  • 2 Schubert, Aleksy
  • 1 Zakrzewski, Jakub

  • Refine by Classification

  • Refine by Keyword
  • 1 Coq theorem prover
  • 1 Hoare logic
  • 1 implicit computational complexity
  • 1 polymorphism
  • 1 program verification
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2012
  • 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 Imprint Privacy Contact