3 Search Results for "Danvy, Olivier"

Document
DOI: 10.4230/OASIcs.EVCS.2023.18
On the Origins of Coccinelle

Authors: Julia Lawall

Published in: OASIcs, Volume 109, Eelco Visser Commemorative Symposium (EVCS 2023)

Abstract
Coccinelle is a program-transformation system for C code. It has been under development since 2005 and has been extensively used on the Linux kernel. The design of Coccinelle was inspired in part by the author’s previous experience in using Stratego/XT, developed by Eelco Visser. This paper reflects on some of Coccinelle’s design choices and their relation to Eelco Visser’s work.
Cite as

Julia Lawall. On the Origins of Coccinelle. In Eelco Visser Commemorative Symposium (EVCS 2023). Open Access Series in Informatics (OASIcs), Volume 109, pp. 18:1-18:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{lawall:OASIcs.EVCS.2023.18,
  author =	{Lawall, Julia},
  title =	{{On the Origins of Coccinelle}},
  booktitle =	{Eelco Visser Commemorative Symposium (EVCS 2023)},
  pages =	{18:1--18:11},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-267-9},
  ISSN =	{2190-6807},
  year =	{2023},
  volume =	{109},
  editor =	{L\"{a}mmel, Ralf and Mosses, Peter D. and Steimann, Friedrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.EVCS.2023.18},
  URN =		{urn:nbn:de:0030-drops-177884},
  doi =		{10.4230/OASIcs.EVCS.2023.18},
  annote =	{Keywords: Linux kernel, Coccinelle, Stratego/XT, program transformation}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2014.72
Typeful Normalization by Evaluation

Authors: Olivier Danvy, Chantal Keller, and Matthias Puech

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

Abstract
We present the first typeful implementation of Normalization by Evaluation for the simply typed lambda-calculus with sums and control operators: we guarantee type preservation and eta-long (modulo commuting conversions), beta-normal forms using only Generalized Algebraic Data Types in a general-purpose programming language, here OCaml; and we account for sums and control operators with Continuation-Passing Style. First, we implement the standard NbE algorithm for the implicational fragment in a typeful way that is correct by construction. We then derive its call-by-value continuation-passing counterpart, that maps a lambda-term with sums and call/cc into a CPS term in normal form, which we express in a typed dedicated syntax. Beyond showcasing the expressive power of GADTs, we emphasize that type inference gives a smooth way to re-derive the encodings of the syntax and typing of normal forms in Continuation-Passing Style.
Cite as

Olivier Danvy, Chantal Keller, and Matthias Puech. Typeful Normalization by Evaluation. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 72-88, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{danvy_et_al:LIPIcs.TYPES.2014.72,
  author =	{Danvy, Olivier and Keller, Chantal and Puech, Matthias},
  title =	{{Typeful Normalization by Evaluation}},
  booktitle =	{20th International Conference on Types for Proofs and Programs (TYPES 2014)},
  pages =	{72--88},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.72},
  URN =		{urn:nbn:de:0030-drops-54921},
  doi =		{10.4230/LIPIcs.TYPES.2014.72},
  annote =	{Keywords: Normalization by Evaluation, Generalized Algebraic Data Types, Continuation-Passing Style, partial evaluation}
}
Document
DOI: 10.4230/DagSemRep.134
Partial Evaluation (Dagstuhl Seminar 9607)

Authors: Olivier Danvy, Robert Glück, and Peter Thiemann

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

Abstract
Cite as

Olivier Danvy, Robert Glück, and Peter Thiemann. Partial Evaluation (Dagstuhl Seminar 9607). Dagstuhl Seminar Report 134, pp. 1-35, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (1996)

Copy BibTex To Clipboard

@TechReport{danvy_et_al:DagSemRep.134,
  author =	{Danvy, Olivier and Gl\"{u}ck, Robert and Thiemann, Peter},
  title =	{{Partial Evaluation (Dagstuhl Seminar 9607)}},
  pages =	{1--35},
  ISSN =	{1619-0203},
  year =	{1996},
  type = 	{Dagstuhl Seminar Report},
  number =	{134},
  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.134},
  URN =		{urn:nbn:de:0030-drops-150218},
  doi =		{10.4230/DagSemRep.134},
}
  • Refine by Author
  • 2 Danvy, Olivier
  • 1 Glück, Robert
  • 1 Keller, Chantal
  • 1 Lawall, Julia
  • 1 Puech, Matthias
  • Show More...

  • Refine by Classification
  • 1 Software and its engineering → Software evolution

  • Refine by Keyword
  • 1 Coccinelle
  • 1 Continuation-Passing Style
  • 1 Generalized Algebraic Data Types
  • 1 Linux kernel
  • 1 Normalization by Evaluation
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 1 1996
  • 1 2015
  • 1 2023

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