8 Search Results for "Garrigue, Jacques"

Document
DOI: 10.4230/LIPIcs.CSL.2026.48
Interpreting Lambda Calculus in Domain-Valued Random Variables

Authors: Robert Furber, Radu Mardare, Prakash Panangaden, and Dana Scott

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
We develop Boolean-valued domain theory and show how the lambda-calculus can be interpreted using domain-valued random variables. We focus on the reflexive domain construction rather than the language and its semantics. We develop the Boolean-valued set theory needed from scratch and then develop Boolean-valued domain theory on top of that. The notions of equality and partial order have to be given Boolean-valued interpretations; when we say that an equation is valid in the model we mean that its interpretation is the top element of the Boolean algebra.
Cite as

Robert Furber, Radu Mardare, Prakash Panangaden, and Dana Scott. Interpreting Lambda Calculus in Domain-Valued Random Variables. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 48:1-48:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{furber_et_al:LIPIcs.CSL.2026.48,
  author =	{Furber, Robert and Mardare, Radu and Panangaden, Prakash and Scott, Dana},
  title =	{{Interpreting Lambda Calculus in Domain-Valued Random Variables}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{48:1--48:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.48},
  URN =		{urn:nbn:de:0030-drops-254734},
  doi =		{10.4230/LIPIcs.CSL.2026.48},
  annote =	{Keywords: lambda calculus, domain theory, random variables}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.33
Solving Guarded Domain Equations in Presheaves over Ordinals and Mechanizing It

Authors: Sergei Stepanenko and Amin Timany

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract
Constructing solutions to recursive domain equations is a well-known, important problem in the study of programs and programming languages. Mathematically speaking, the problem is finding a fixed point (up to isomorphism) of a suitable functor over a suitable category. A particularly useful instance, inspired by the step-indexing technique, is where the functor is over (a subcategory of) the category of presheaves over the ordinal ω and the functors are locally-contractive, also known as guarded functors. This corresponds to step-indexing over natural numbers. However, for certain problems, e.g., when dealing with infinite non-determinism, one needs to employ trans-finite step-indexing, i.e., consider presheaf categories over higher ordinals. Prior work on trans-finite step-indexing either only considers a very narrow class of functors over a particularly restricted subcategory of presheaves over higher ordinals, or treats the problem very generally working with sheaves over an arbitrary complete Heyting algebra with a well-founded basis. In this paper we present a solution to the guarded domain equations problem over all guarded functors over the category of presheaves over ordinal numbers, as well as its mechanization in the Rocq Prover. As the categories of sheaves and presheaves over ordinals are equivalent, our main contribution is simplifying prior work from the setting of the category of sheaves to the setting of the category of presheaves and mechanizing it - presheaves are more amenable to mechanization in a proof assistant.
Cite as

Sergei Stepanenko and Amin Timany. Solving Guarded Domain Equations in Presheaves over Ordinals and Mechanizing It. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 33:1-33:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{stepanenko_et_al:LIPIcs.FSCD.2025.33,
  author =	{Stepanenko, Sergei and Timany, Amin},
  title =	{{Solving Guarded Domain Equations in Presheaves over Ordinals and Mechanizing It}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{33:1--33:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.33},
  URN =		{urn:nbn:de:0030-drops-236486},
  doi =		{10.4230/LIPIcs.FSCD.2025.33},
  annote =	{Keywords: Domain Equations, Guarded Fixed Points, Fixed Points, Category Theory, Rocq, Presheaves, Ordinals}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2025.24
Fair Termination of Asynchronous Binary Sessions

Authors: Luca Padovani and Gianluigi Zavattaro

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract
We study a theory of asynchronous session types ensuring that well-typed processes terminate under a suitable fairness assumption. Fair termination entails starvation freedom and orphan message freedom namely that all messages, including those that are produced early taking advantage of asynchrony, are eventually consumed. The theory is based on a novel fair asynchronous subtyping relation for session types that is coarser than the existing ones. The type system is also the first of its kind that is firmly rooted in linear logic: fair asynchronous subtyping is incorporated as a natural generalization of the cut and axiom rules of linear logic and asynchronous communication is modeled through a suitable set of commuting conversions and of deep cut reductions in linear logic proofs.
Cite as

Luca Padovani and Gianluigi Zavattaro. Fair Termination of Asynchronous Binary Sessions. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 24:1-24:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{padovani_et_al:LIPIcs.ECOOP.2025.24,
  author =	{Padovani, Luca and Zavattaro, Gianluigi},
  title =	{{Fair Termination of Asynchronous Binary Sessions}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{24:1--24:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-373-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{333},
  editor =	{Aldrich, Jonathan and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.24},
  URN =		{urn:nbn:de:0030-drops-233169},
  doi =		{10.4230/LIPIcs.ECOOP.2025.24},
  annote =	{Keywords: Binary sessions, fair asynchronous subtyping, fair termination, linear logic}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2025.2
The Algebra of Patterns

Authors: David Binder and Lean Ermantraut

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract
Pattern matching is a popular feature in functional, imperative and object-oriented programming languages. Language designers should therefore invest effort in a good design for pattern matching. Most languages choose a first-match semantics for pattern matching; that is, clauses are tried in the order in which they appear in the program until the first one matches. As a consequence, the order in which the clauses appear cannot be arbitrarily changed, which results in a less declarative programming model. The declarative alternative to this is an order-independent semantics for pattern matching, which is not implemented in most programming languages since it requires more verbose patterns. The reason for this verbosity is that the syntax of patterns is usually not expressive enough to express the complement of a pattern. In this paper, we show a principled way to make order-independent pattern matching practical. Our solution consists of two parts: First, we introduce a boolean algebra of patterns which can express the complement of a pattern. Second, we introduce default clauses to pattern matches. These default clauses capture the essential idea of a fallthrough case without sacrificing the property of order-independence.
Cite as

David Binder and Lean Ermantraut. The Algebra of Patterns. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 2:1-2:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{binder_et_al:LIPIcs.ECOOP.2025.2,
  author =	{Binder, David and Ermantraut, Lean},
  title =	{{The Algebra of Patterns}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{2:1--2:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-373-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{333},
  editor =	{Aldrich, Jonathan and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.2},
  URN =		{urn:nbn:de:0030-drops-232959},
  doi =		{10.4230/LIPIcs.ECOOP.2025.2},
  annote =	{Keywords: functional programming, pattern matching, algebraic data types, equational reasoning}
}
Artifact
Software
DOI: 10.4230/artifacts.22446
QECC: Quantum Computation and Error-Correcting Codes

Authors: Jacques Garrigue and Takafumi Saikawa

Abstract
Cite as

Jacques Garrigue, Takafumi Saikawa. QECC: Quantum Computation and Error-Correcting Codes (Software). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-22446,
   title = {{QECC: Quantum Computation and Error-Correcting Codes}}, 
   author = {Garrigue, Jacques and Saikawa, Takafumi},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:d4d158675180ee276e730bd7f67a9122a6472eb3;origin=https://github.com/t6s/qecc;visit=swh:1:snp:98c582f9ca38ec1ef707cc25a4ef8f23befe0386;anchor=swh:1:rev:afc45f0ce1b3258fbf0c9469085ff8749de14a2a}{\texttt{swh:1:dir:d4d158675180ee276e730bd7f67a9122a6472eb3}} (visited on 2024-11-28)},
   url = {https://github.com/t6s/qecc},
   doi = {10.4230/artifacts.22446},
}
Document
DOI: 10.4230/LIPIcs.ITP.2024.15
Typed Compositional Quantum Computation with Lenses

Authors: Jacques Garrigue and Takafumi Saikawa

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract
We propose a type-theoretic framework for describing and proving properties of quantum computations, in particular those presented as quantum circuits. Our proposal is based on an observation that, in the polymorphic type system of Coq, currying on quantum states allows one to apply quantum gates directly inside a complex circuit. By introducing a discrete notion of lens to control this currying, we are further able to separate the combinatorics of the circuit structure from the computational content of gates. We apply our development to define quantum circuits recursively from the bottom up, and prove their correctness compositionally.
Cite as

Jacques Garrigue and Takafumi Saikawa. Typed Compositional Quantum Computation with Lenses. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 15:1-15:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{garrigue_et_al:LIPIcs.ITP.2024.15,
  author =	{Garrigue, Jacques and Saikawa, Takafumi},
  title =	{{Typed Compositional Quantum Computation with Lenses}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{15:1--15:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.15},
  URN =		{urn:nbn:de:0030-drops-207431},
  doi =		{10.4230/LIPIcs.ITP.2024.15},
  annote =	{Keywords: quantum programming, semantics, lens, currying, Coq, MathComp}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2020.9
Multiparty Session Programming With Global Protocol Combinators

Authors: Keigo Imai, Rumyana Neykova, Nobuko Yoshida, and Shoji Yuen

Published in: LIPIcs, Volume 166, 34th European Conference on Object-Oriented Programming (ECOOP 2020)

Abstract
Multiparty Session Types (MPST) is a typing discipline for communication protocols. It ensures the absence of communication errors and deadlocks for well-typed communicating processes. The state-of-the-art implementations of the MPST theory rely on (1) runtime linearity checks to ensure correct usage of communication channels and (2) external domain-specific languages for specifying and verifying multiparty protocols. To overcome these limitations, we propose a library for programming with global combinators - a set of functions for writing and verifying multiparty protocols in OCaml. Local behaviours for all processes in a protocol are inferred at once from a global combinator. We formalise global combinators and prove a sound realisability of global combinators - a well-typed global combinator derives a set of local types, by which typed endpoint programs can ensure type and communication safety. Our approach enables fully-static verification and implementation of the whole protocol, from the protocol specification to the process implementations, to happen in the same language. We compare our implementation to untyped and continuation-passing style implementations, and demonstrate its expressiveness by implementing a plethora of protocols. We show our library can interoperate with existing libraries and services, implementing DNS (Domain Name Service) protocol and the OAuth (Open Authentication) protocol.
Cite as

Keigo Imai, Rumyana Neykova, Nobuko Yoshida, and Shoji Yuen. Multiparty Session Programming With Global Protocol Combinators. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 9:1-9:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{imai_et_al:LIPIcs.ECOOP.2020.9,
  author =	{Imai, Keigo and Neykova, Rumyana and Yoshida, Nobuko and Yuen, Shoji},
  title =	{{Multiparty Session Programming With Global Protocol Combinators}},
  booktitle =	{34th European Conference on Object-Oriented Programming (ECOOP 2020)},
  pages =	{9:1--9:30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-154-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{166},
  editor =	{Hirschfeld, Robert and Pape, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2020.9},
  URN =		{urn:nbn:de:0030-drops-131662},
  doi =		{10.4230/LIPIcs.ECOOP.2020.9},
  annote =	{Keywords: Multiparty Session Types, Communication Protocol, Concurrent and Distributed Programming, OCaml}
}
Document
DOI: 10.4230/LIPIcs.ITP.2019.5
Proving Tree Algorithms for Succinct Data Structures

Authors: Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, and Kazunari Tanaka

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)

Abstract
Succinct data structures give space-efficient representations of large amounts of data without sacrificing performance. They rely on cleverly designed data representations and algorithms. We present here the formalization in Coq/SSReflect of two different tree-based succinct representations and their accompanying algorithms. One is the Level-Order Unary Degree Sequence, which encodes the structure of a tree in breadth-first order as a sequence of bits, where access operations can be defined in terms of Rank and Select, which work in constant time for static bit sequences. The other represents dynamic bit sequences as binary balanced trees, where Rank and Select present a low logarithmic overhead compared to their static versions, and with efficient insertion and deletion. The two can be stacked to provide a dynamic representation of dictionaries for instance. While both representations are well-known, we believe this to be their first formalization and a needed step towards provably-safe implementations of big data.
Cite as

Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, and Kazunari Tanaka. Proving Tree Algorithms for Succinct Data Structures. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 5:1-5:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{affeldt_et_al:LIPIcs.ITP.2019.5,
  author =	{Affeldt, Reynald and Garrigue, Jacques and Qi, Xuanrui and Tanaka, Kazunari},
  title =	{{Proving Tree Algorithms for Succinct Data Structures}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{5:1--5:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{Harrison, John and O'Leary, John and Tolmach, Andrew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.5},
  URN =		{urn:nbn:de:0030-drops-110609},
  doi =		{10.4230/LIPIcs.ITP.2019.5},
  annote =	{Keywords: Coq, small-scale reflection, succinct data structures, LOUDS, bit vectors, self balancing trees}
}
  • Refine by Type
  • 7 Document/PDF
  • 4 Document/HTML
  • 1 Artifact

  • Refine by Publication Year
  • 1 2026
  • 3 2025
  • 2 2024
  • 1 2020
  • 1 2019

  • Refine by Author
  • 3 Garrigue, Jacques
  • 2 Saikawa, Takafumi
  • 1 Affeldt, Reynald
  • 1 Binder, David
  • 1 Ermantraut, Lean
  • Show More...

  • Refine by Series/Journal
  • 7 LIPIcs

  • Refine by Classification
  • 2 Theory of computation → Denotational semantics
  • 2 Theory of computation → Lambda calculus
  • 2 Theory of computation → Type structures
  • 2 Theory of computation → Type theory
  • 1 Software and its engineering → Concurrent programming structures
  • Show More...

  • Refine by Keyword
  • 2 Coq
  • 1 Binary sessions
  • 1 Category Theory
  • 1 Communication Protocol
  • 1 Concurrent and Distributed Programming
  • 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