2 Search Results for "Pagano, Miguel"

Document
DOI: 10.4230/LIPIcs.TYPES.2024.5
Implementing a Type Theory with Observational Equality, Using Normalisation by Evaluation

Authors: Matthew Sirman, Meven Lennon-Bertrand, and Neel Krishnaswami

Published in: LIPIcs, Volume 336, 30th International Conference on Types for Proofs and Programs (TYPES 2024)

Abstract
We report on an experimental implementation in Haskell of a dependent type theory featuring an observational equality type, based on Pujet et al.’s CCobs. We use normalisation by evaluation to produce an efficient normalisation function, which is used to implement a bidirectional type checker. To allow for greater expressivity, we extend the core CCobs calculus with quotient types and inductive types. To make the system usable, we explore various proof-assistant features, notably a rudimentary version of a "hole" system similar to Agda’s. While rather crude, this experience should inform other, more substantial implementation efforts of observational equality.
Cite as

Matthew Sirman, Meven Lennon-Bertrand, and Neel Krishnaswami. Implementing a Type Theory with Observational Equality, Using Normalisation by Evaluation. In 30th International Conference on Types for Proofs and Programs (TYPES 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 336, pp. 5:1-5:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{sirman_et_al:LIPIcs.TYPES.2024.5,
  author =	{Sirman, Matthew and Lennon-Bertrand, Meven and Krishnaswami, Neel},
  title =	{{Implementing a Type Theory with Observational Equality, Using Normalisation by Evaluation}},
  booktitle =	{30th International Conference on Types for Proofs and Programs (TYPES 2024)},
  pages =	{5:1--5:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-376-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{336},
  editor =	{M{\o}gelberg, Rasmus Ejlers and van den Berg, Benno},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2024.5},
  URN =		{urn:nbn:de:0030-drops-233673},
  doi =		{10.4230/LIPIcs.TYPES.2024.5},
  annote =	{Keywords: Dependent type theory, Bidirectional typing, Observational equality, Normalisation by evaluation}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2013.230
A Certified Extension of the Krivine Machine for a Call-by-Name Higher-Order Imperative Language

Authors: Leonardo Rodríguez, Daniel Fridlender, and Miguel Pagano

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

Abstract
In this paper we present a compiler that translates programs from an imperative higher-order language into a sequence of instructions for an abstract machine. We consider an extension of the Krivine machine for the call-by-name lambda calculus, which includes strict operators and imperative features. We show that the compiler is correct with respect to the big-step semantics of our language, both for convergent and divergent programs.
Cite as

Leonardo Rodríguez, Daniel Fridlender, and Miguel Pagano. A Certified Extension of the Krivine Machine for a Call-by-Name Higher-Order Imperative Language. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 230-250, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{rodriguez_et_al:LIPIcs.TYPES.2013.230,
  author =	{Rodr{\'\i}guez, Leonardo and Fridlender, Daniel and Pagano, Miguel},
  title =	{{A Certified Extension of the Krivine Machine for a Call-by-Name Higher-Order Imperative Language}},
  booktitle =	{19th International Conference on Types for Proofs and Programs (TYPES 2013)},
  pages =	{230--250},
  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.230},
  URN =		{urn:nbn:de:0030-drops-46343},
  doi =		{10.4230/LIPIcs.TYPES.2013.230},
  annote =	{Keywords: Abstract Machines, Compiler Correctness, Big-step semantics}
}
  • Refine by Type
  • 2 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2025
  • 1 2014

  • Refine by Author
  • 1 Fridlender, Daniel
  • 1 Krishnaswami, Neel
  • 1 Lennon-Bertrand, Meven
  • 1 Pagano, Miguel
  • 1 Rodríguez, Leonardo
  • Show More...

  • Refine by Series/Journal
  • 2 LIPIcs

  • Refine by Classification
  • 1 Software and its engineering → Functional languages
  • 1 Theory of computation → Denotational semantics
  • 1 Theory of computation → Type theory

  • Refine by Keyword
  • 1 Abstract Machines
  • 1 Bidirectional typing
  • 1 Big-step semantics
  • 1 Compiler Correctness
  • 1 Dependent type theory
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact