4 Search Results for "Allais, Guillaume"


Document
Type Theory as a Language Workbench

Authors: Jan de Muijnck-Hughes, Guillaume Allais, and Edwin Brady

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


Abstract
Language Workbenches offer language designers an expressive environment in which to create their Domain Specific Languages (DSLs). Similarly, research into mechanised meta-theory has shown how dependently typed languages provide expressive environments to formalise and study DSLs and their meta-theoretical properties. But can we claim that dependently typed languages qualify as language workbenches? We argue yes! We have developed an exemplar DSL called Vélo that showcases not only dependently typed techniques to realise and manipulate Intermediate Representations (IRs), but that dependently typed languages make fine language workbenches. Vélo is a simple verified language with well-typed holes and comes with a complete compiler pipeline: parser, elaborator, REPL, evaluator, and compiler passes. Specifically, we describe our design choices for well-typed IR design that includes support for well-typed holes, how CSE is achieved in a well-typed setting, and how the mechanised type-soundness proof for Vélo is the source of the evaluator.

Cite as

Jan de Muijnck-Hughes, Guillaume Allais, and Edwin Brady. Type Theory as a Language Workbench. In Eelco Visser Commemorative Symposium (EVCS 2023). Open Access Series in Informatics (OASIcs), Volume 109, pp. 9:1-9:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{demuijnckhughes_et_al:OASIcs.EVCS.2023.9,
  author =	{de Muijnck-Hughes, Jan and Allais, Guillaume and Brady, Edwin},
  title =	{{Type Theory as a Language Workbench}},
  booktitle =	{Eelco Visser Commemorative Symposium (EVCS 2023)},
  pages =	{9:1--9:13},
  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.9},
  URN =		{urn:nbn:de:0030-drops-177797},
  doi =		{10.4230/OASIcs.EVCS.2023.9},
  annote =	{Keywords: dependent types, language workbenches, idris2, dsl, edsl, intrinsically scoped, well typed, co-De Bruijn}
}
Document
Guarded Recursion in Agda via Sized Types

Authors: Niccolò Veltri and Niels van der Weide

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


Abstract
In type theory, programming and reasoning with possibly non-terminating programs and potentially infinite objects is achieved using coinductive types. Recursively defined programs of these types need to be productive to guarantee the consistency of the type system. Proof assistants such as Agda and Coq traditionally employ strict syntactic productivity checks, which often make programming with coinductive types convoluted. One way to overcome this issue is by encoding productivity at the level of types so that the type system forbids the implementation of non-productive corecursive programs. In this paper we compare two different approaches to type-based productivity: guarded recursion and sized types. More specifically, we show how to simulate guarded recursion in Agda using sized types. We formalize the syntax of a simple type theory for guarded recursion, which is a variant of Atkey and McBride’s calculus for productive coprogramming. Then we give a denotational semantics using presheaves over the preorder of sizes. Sized types are fundamentally used to interpret the characteristic features of guarded recursion, notably the fixpoint combinator.

Cite as

Niccolò Veltri and Niels van der Weide. Guarded Recursion in Agda via Sized Types. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 32:1-32:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{veltri_et_al:LIPIcs.FSCD.2019.32,
  author =	{Veltri, Niccol\`{o} and van der Weide, Niels},
  title =	{{Guarded Recursion in Agda via Sized Types}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{32:1--32:19},
  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.32},
  URN =		{urn:nbn:de:0030-drops-105391},
  doi =		{10.4230/LIPIcs.FSCD.2019.32},
  annote =	{Keywords: guarded recursion, type theory, semantics, coinduction, sized types}
}
Document
Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic

Authors: Guillaume Allais

Published in: LIPIcs, Volume 104, 23rd International Conference on Types for Proofs and Programs (TYPES 2017)


Abstract
We start from an untyped, well-scoped lambda-calculus and introduce a bidirectional typing relation corresponding to a Multiplicative-Additive Intuitionistic Linear Logic. We depart from typical presentations to adopt one that is well-suited to the intensional setting of Martin-Löf Type Theory. This relation is based on the idea that a linear term consumes some of the resources available in its context whilst leaving behind leftovers which can then be fed to another program. Concretely, this means that typing derivations have both an input and an output context. This leads to a notion of weakening (the extra resources added to the input context come out unchanged in the output one), a rather direct proof of stability under substitution, an analogue of the frame rule of separation logic showing that the state of unused resources can be safely ignored, and a proof that typechecking is decidable. Finally, we demonstrate that this alternative formalization is sound and complete with respect to a more traditional representation of Intuitionistic Linear Logic. The work has been fully formalised in Agda, commented source files are provided as additional material available at https://github.com/gallais/typing-with-leftovers.

Cite as

Guillaume Allais. Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic. In 23rd International Conference on Types for Proofs and Programs (TYPES 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 104, pp. 1:1-1:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{allais:LIPIcs.TYPES.2017.1,
  author =	{Allais, Guillaume},
  title =	{{Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic}},
  booktitle =	{23rd International Conference on Types for Proofs and Programs (TYPES 2017)},
  pages =	{1:1--1:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-071-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{104},
  editor =	{Abel, Andreas and Nordvall Forsberg, Fredrik and Kaposi, Ambrus},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2017.1},
  URN =		{urn:nbn:de:0030-drops-100490},
  doi =		{10.4230/LIPIcs.TYPES.2017.1},
  annote =	{Keywords: Type System, Bidirectional, Linear Logic, Agda}
}
Document
On the Formalization of Termination Techniques based on Multiset Orderings

Authors: René Thiemann, Guillaume Allais, and Julian Nagele

Published in: LIPIcs, Volume 15, 23rd International Conference on Rewriting Techniques and Applications (RTA'12) (2012)


Abstract
Multiset orderings are a key ingredient in certain termination techniques like the recursive path ordering and a variant of size-change termination. In order to integrate these techniques in a certifier for termination proofs, we have added them to the Isabelle Formalization of Rewriting. To this end, it was required to extend the existing formalization on multiset orderings towards a generalized multiset ordering. Afterwards, the soundness proofs of both techniques have been established, although only after fixing some definitions. Concerning efficiency, it is known that the search for suitable parameters for both techniques is NP-hard. We show that checking the correct application of the techniques--where all parameters are provided--is also NP-hard, since the problem of deciding the generalized multiset ordering is NP-hard.

Cite as

René Thiemann, Guillaume Allais, and Julian Nagele. On the Formalization of Termination Techniques based on Multiset Orderings. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 339-354, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)


Copy BibTex To Clipboard

@InProceedings{thiemann_et_al:LIPIcs.RTA.2012.339,
  author =	{Thiemann, Ren\'{e} and Allais, Guillaume and Nagele, Julian},
  title =	{{On the Formalization of Termination Techniques based on Multiset Orderings}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{339--354},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.339},
  URN =		{urn:nbn:de:0030-drops-35029},
  doi =		{10.4230/LIPIcs.RTA.2012.339},
  annote =	{Keywords: formalization, term rewriting, termination, orderings}
}
  • Refine by Author
  • 3 Allais, Guillaume
  • 1 Brady, Edwin
  • 1 Nagele, Julian
  • 1 Thiemann, René
  • 1 Veltri, Niccolò
  • Show More...

  • Refine by Classification
  • 3 Theory of computation → Type theory
  • 1 Software and its engineering → Compilers
  • 1 Software and its engineering → Domain specific languages
  • 1 Software and its engineering → Formal language definitions
  • 1 Software and its engineering → Functional languages
  • Show More...

  • Refine by Keyword
  • 1 Agda
  • 1 Bidirectional
  • 1 Linear Logic
  • 1 Type System
  • 1 co-De Bruijn
  • Show More...

  • Refine by Type
  • 4 document

  • Refine by Publication Year
  • 2 2019
  • 1 2012
  • 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