3 Search Results for "Pierce, Benjamin"

Document
DOI: 10.4230/LIPIcs.ITP.2021.32
Verifying an HTTP Key-Value Server with Interaction Trees and VST

Authors: Hengchu Zhang, Wolf Honoré, Nicolas Koh, Yao Li, Yishuai Li, Li-Yao Xia, Lennart Beringer, William Mansky, Benjamin Pierce, and Steve Zdancewic

Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)

Abstract
We present a networked key-value server, implemented in C and formally verified in Coq. The server interacts with clients using a subset of the HTTP/1.1 protocol and is specified and verified using interaction trees and the Verified Software Toolchain. The codebase includes a reusable and fully verified C string library that provides 17 standard POSIX string functions and 17 general purpose non-POSIX string functions. For the KVServer socket system calls, we establish a refinement relation between specifications at user-space level and at CertiKOS kernel-space level.
Cite as

Hengchu Zhang, Wolf Honoré, Nicolas Koh, Yao Li, Yishuai Li, Li-Yao Xia, Lennart Beringer, William Mansky, Benjamin Pierce, and Steve Zdancewic. Verifying an HTTP Key-Value Server with Interaction Trees and VST. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 32:1-32:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{zhang_et_al:LIPIcs.ITP.2021.32,
  author =	{Zhang, Hengchu and Honor\'{e}, Wolf and Koh, Nicolas and Li, Yao and Li, Yishuai and Xia, Li-Yao and Beringer, Lennart and Mansky, William and Pierce, Benjamin and Zdancewic, Steve},
  title =	{{Verifying an HTTP Key-Value Server with Interaction Trees and VST}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{32:1--32:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.32},
  URN =		{urn:nbn:de:0030-drops-139273},
  doi =		{10.4230/LIPIcs.ITP.2021.32},
  annote =	{Keywords: formal verification, Coq, HTTP, deep specification}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2019.28
The Delta-calculus: Syntax and Types

Authors: Luigi Liquori and Claude Stolze

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

Abstract
We present the Delta-calculus, an explicitly typed lambda-calculus with strong pairs, projections and explicit type coercions. The calculus can be parametrized with different intersection type theories T, e.g. the Coppo-Dezani, the Coppo-Dezani-Sallé, the Coppo-Dezani-Venneri and the Barendregt-Coppo-Dezani ones, producing a family of Delta-calculi with related intersection typed systems. We prove the main properties like Church-Rosser, unicity of type, subject reduction, strong normalization, decidability of type checking and type reconstruction. We state the relationship between the intersection type assignment systems à la Curry and the corresponding intersection typed systems à la Church by means of an essence function translating an explicitly typed Delta-term into a pure lambda-term one. We finally translate a Delta-term with type coercions into an equivalent one without them; the translation is proved to be coherent because its essence is the identity. The generic Delta-calculus can be parametrized to take into account other intersection type theories as the ones in the Barendregt et al. book.
Cite as

Luigi Liquori and Claude Stolze. The Delta-calculus: Syntax and Types. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 28:1-28:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{liquori_et_al:LIPIcs.FSCD.2019.28,
  author =	{Liquori, Luigi and Stolze, Claude},
  title =	{{The Delta-calculus: Syntax and Types}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{28:1--28:20},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.28},
  URN =		{urn:nbn:de:0030-drops-105354},
  doi =		{10.4230/LIPIcs.FSCD.2019.28},
  annote =	{Keywords: intersection types, lambda calculus \`{a} la Church and \`{a} la Curry, proof-functional logics}
}
Document
DOI: 10.4230/DagSemRep.164
High-Level Concurrent Languages (Dagstuhl Seminar 97041)

Authors: Kohei Honda, Martin Odersky, Benjamin Pierce, Gert Smolla, and Philip Wadler

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

Kohei Honda, Martin Odersky, Benjamin Pierce, Gert Smolla, and Philip Wadler. High-Level Concurrent Languages (Dagstuhl Seminar 97041). Dagstuhl Seminar Report 164, pp. 1-20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (1997)

Copy BibTex To Clipboard

@TechReport{honda_et_al:DagSemRep.164,
  author =	{Honda, Kohei and Odersky, Martin and Pierce, Benjamin and Smolla, Gert and Wadler, Philip},
  title =	{{High-Level Concurrent Languages (Dagstuhl Seminar 97041)}},
  pages =	{1--20},
  ISSN =	{1619-0203},
  year =	{1997},
  type = 	{Dagstuhl Seminar Report},
  number =	{164},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemRep.164},
  URN =		{urn:nbn:de:0030-drops-150514},
  doi =		{10.4230/DagSemRep.164},
}
  • Refine by Author
  • 2 Pierce, Benjamin
  • 1 Beringer, Lennart
  • 1 Honda, Kohei
  • 1 Honoré, Wolf
  • 1 Koh, Nicolas
  • Show More...

  • Refine by Classification
  • 1 Theory of computation → Lambda calculus
  • 1 Theory of computation → Program specifications
  • 1 Theory of computation → Program verification
  • 1 Theory of computation → Separation logic
  • 1 Theory of computation → Type theory

  • Refine by Keyword
  • 1 Coq
  • 1 HTTP
  • 1 deep specification
  • 1 formal verification
  • 1 intersection types
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 1 1997
  • 1 2019
  • 1 2021

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