25 Search Results for "Mahboubi, Assia"


Volume

LIPIcs, Volume 175

25th International Conference on Types for Proofs and Programs (TYPES 2019)

TYPES 2019, June 11-14, 2019, Oslo, Norway

Editors: Marc Bezem and Assia Mahboubi

Document
The Kleene-Post and Post’s Theorem in the Calculus of Inductive Constructions

Authors: Yannick Forster, Dominik Kirst, and Niklas Mück

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)


Abstract
The Kleene-Post theorem and Post’s theorem are two central and historically important results in the development of oracle computability theory, clarifying the structure of Turing reducibility degrees. They state, respectively, that there are incomparable Turing degrees and that the arithmetical hierarchy is connected to the relativised form of the halting problem defined via Turing jumps. We study these two results in the calculus of inductive constructions (CIC), the constructive type theory underlying the Coq proof assistant. CIC constitutes an ideal foundation for the formalisation of computability theory for two reasons: First, like in other constructive foundations, computable functions can be treated via axioms as a purely synthetic notion rather than being defined in terms of a concrete analytic model of computation such as Turing machines. Furthermore and uniquely, CIC allows consistently assuming classical logic via the law of excluded middle or weaker variants on top of axioms for synthetic computability, enabling both fully classical developments and taking the perspective of constructive reverse mathematics on computability theory. In the present paper, we give a fully constructive construction of two Turing-incomparable degrees à la Kleene-Post and observe that the classical content of Post’s theorem seems to be related to the arithmetical hierarchy of the law of excluded middle due to Akama et. al. Technically, we base our investigation on a previously studied notion of synthetic oracle computability and contribute the first consistency proof of a suitable enumeration axiom. All results discussed in the paper are mechanised and contributed to the Coq library of synthetic computability.

Cite as

Yannick Forster, Dominik Kirst, and Niklas Mück. The Kleene-Post and Post’s Theorem in the Calculus of Inductive Constructions. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 29:1-29:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{forster_et_al:LIPIcs.CSL.2024.29,
  author =	{Forster, Yannick and Kirst, Dominik and M\"{u}ck, Niklas},
  title =	{{The Kleene-Post and Post’s Theorem in the Calculus of Inductive Constructions}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{29:1--29:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.29},
  URN =		{urn:nbn:de:0030-drops-196728},
  doi =		{10.4230/LIPIcs.CSL.2024.29},
  annote =	{Keywords: Constructive mathematics, Computability theory, Logical foundations, Constructive type theory, Interactive theorem proving, Coq proof assistant}
}
Document
A First Order Theory of Diagram Chasing

Authors: Assia Mahboubi and Matthieu Piquerez

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)


Abstract
This paper discusses the formalization of proofs "by diagram chasing", a standard technique for proving properties in abelian categories. We discuss how the essence of diagram chases can be captured by a simple many-sorted first-order theory, and we study the models and decidability of this theory. The longer-term motivation of this work is the design of a computer-aided instrument for writing reliable proofs in homological algebra, based on interactive theorem provers.

Cite as

Assia Mahboubi and Matthieu Piquerez. A First Order Theory of Diagram Chasing. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 38:1-38:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{mahboubi_et_al:LIPIcs.CSL.2024.38,
  author =	{Mahboubi, Assia and Piquerez, Matthieu},
  title =	{{A First Order Theory of Diagram Chasing}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{38:1--38:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.38},
  URN =		{urn:nbn:de:0030-drops-196817},
  doi =		{10.4230/LIPIcs.CSL.2024.38},
  annote =	{Keywords: Diagram chasing, formal proofs, abelian categories, decidability}
}
Document
Invited Talk
Machine-Checked Computational Mathematics (Invited Talk)

Authors: Assia Mahboubi

Published in: LIPIcs, Volume 270, 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)


Abstract
This talk shall discuss the potential impact of formal methods, and in particular, of interactive theorem proving, on computational mathematics. Geared with increasingly fast computer algebra libraries and scientific computing software, computers have become amazing instruments for mathematical guesswork. In fact, computer calculations are even sometimes used to substantiate actual reasoning steps in proofs, later published in major venues of the mathematical literature. Yet surprisingly, little of the now standard techniques available today for verifying critical software (e.g., cryptographic components, airborne commands, etc.) have been applied to the programs used to produce mathematics. In this talk, we propose to discuss this state of affairs.

Cite as

Assia Mahboubi. Machine-Checked Computational Mathematics (Invited Talk). In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, p. 5:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{mahboubi:LIPIcs.CALCO.2023.5,
  author =	{Mahboubi, Assia},
  title =	{{Machine-Checked Computational Mathematics}},
  booktitle =	{10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)},
  pages =	{5:1--5:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-287-7},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{270},
  editor =	{Baldan, Paolo and de Paiva, Valeria},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.5},
  URN =		{urn:nbn:de:0030-drops-188024},
  doi =		{10.4230/LIPIcs.CALCO.2023.5},
  annote =	{Keywords: Type theory, computer algebra, interactive theorem proving}
}
Document
Use and Abuse of Instance Parameters in the Lean Mathematical Library

Authors: Anne Baanen

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)


Abstract
The Lean mathematical library mathlib features extensive use of the typeclass pattern for organising mathematical structures, based on Lean’s mechanism of instance parameters. Related mechanisms for typeclasses are available in other provers including Agda, Coq and Isabelle with varying degrees of adoption. This paper analyses representative examples of design patterns involving instance parameters in the current Lean 3 version of mathlib, focussing on complications arising at scale and how the mathlib community deals with them.

Cite as

Anne Baanen. Use and Abuse of Instance Parameters in the Lean Mathematical Library. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 4:1-4:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{baanen:LIPIcs.ITP.2022.4,
  author =	{Baanen, Anne},
  title =	{{Use and Abuse of Instance Parameters in the Lean Mathematical Library}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{4:1--4:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.4},
  URN =		{urn:nbn:de:0030-drops-167131},
  doi =		{10.4230/LIPIcs.ITP.2022.4},
  annote =	{Keywords: formalization of mathematics, dependent type theory, typeclasses, algebraic hierarchy, Lean prover}
}
Document
Reflexive Tactics for Algebra, Revisited

Authors: Kazuhiko Sakaguchi

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)


Abstract
Computational reflection allows us to turn verified decision procedures into efficient automated reasoning tools in proof assistants. The typical applications of such methodology include decidable algebraic theories such as equational theories of commutative rings and lattices. However, such existing tools are known not to cooperate with packed classes, a methodology to define mathematical structures in dependent type theory, that allows for the sharing of vocabulary across the inheritance hierarchy. Moreover, such tools do not support homomorphisms whose domain and codomain types may differ. This paper demonstrates how to implement reflexive tactics that support packed classes and homomorphisms. As applications of our methodology, we adapt the ring and field tactics of Coq to the commutative ring and field structures of the Mathematical Components library, and apply the resulting tactics to the formal proof of the irrationality of ζ(3) by Chyzak, Mahboubi, and Sibut-Pinote. As a result, the lines of code in the proof scripts have been reduced by 8%, and the time required for proof checking has been decreased by 27%.

Cite as

Kazuhiko Sakaguchi. Reflexive Tactics for Algebra, Revisited. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 29:1-29:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{sakaguchi:LIPIcs.ITP.2022.29,
  author =	{Sakaguchi, Kazuhiko},
  title =	{{Reflexive Tactics for Algebra, Revisited}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{29:1--29:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.29},
  URN =		{urn:nbn:de:0030-drops-167385},
  doi =		{10.4230/LIPIcs.ITP.2022.29},
  annote =	{Keywords: Coq, Elpi, \lambdaProlog, Mathematical Components, algebraic structures, packed classes, canonical structures, proof by reflection}
}
Document
Gardening with the Pythia A Model of Continuity in a Dependent Setting

Authors: Martin Baillon, Assia Mahboubi, and Pierre-Marie Pédrot

Published in: LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)


Abstract
We generalize to a rich dependent type theory a proof originally developed by Escardó that all System 𝚃 functionals are continuous. It relies on the definition of a syntactic model of Baclofen Type Theory, a type theory where dependent elimination must be strict, into the Calculus of Inductive Constructions. The model is given by three translations: the axiom translation, that adds an oracle to the context; the branching translation, based on the dialogue monad, turning every type into a tree; and finally, a layer of algebraic binary parametricity, binding together the two translations. In the resulting type theory, every function f : (ℕ → ℕ) → ℕ is externally continuous.

Cite as

Martin Baillon, Assia Mahboubi, and Pierre-Marie Pédrot. Gardening with the Pythia A Model of Continuity in a Dependent Setting. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 5:1-5:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{baillon_et_al:LIPIcs.CSL.2022.5,
  author =	{Baillon, Martin and Mahboubi, Assia and P\'{e}drot, Pierre-Marie},
  title =	{{Gardening with the Pythia A Model of Continuity in a Dependent Setting}},
  booktitle =	{30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  pages =	{5:1--5:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-218-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{216},
  editor =	{Manea, Florin and Simpson, Alex},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.5},
  URN =		{urn:nbn:de:0030-drops-157256},
  doi =		{10.4230/LIPIcs.CSL.2022.5},
  annote =	{Keywords: Type theory, continuity, syntactic model}
}
Document
Unsolvability of the Quintic Formalized in Dependent Type Theory

Authors: Sophie Bernard, Cyril Cohen, Assia Mahboubi, and Pierre-Yves Strub

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


Abstract
In this paper, we describe an axiom-free Coq formalization that there does not exists a general method for solving by radicals polynomial equations of degree greater than 4. This development includes a proof of Galois' Theorem of the equivalence between solvable extensions and extensions solvable by radicals. The unsolvability of the general quintic follows from applying this theorem to a well chosen polynomial with unsolvable Galois group.

Cite as

Sophie Bernard, Cyril Cohen, Assia Mahboubi, and Pierre-Yves Strub. Unsolvability of the Quintic Formalized in Dependent Type Theory. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{bernard_et_al:LIPIcs.ITP.2021.8,
  author =	{Bernard, Sophie and Cohen, Cyril and Mahboubi, Assia and Strub, Pierre-Yves},
  title =	{{Unsolvability of the Quintic Formalized in Dependent Type Theory}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{8:1--8:18},
  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.8},
  URN =		{urn:nbn:de:0030-drops-139038},
  doi =		{10.4230/LIPIcs.ITP.2021.8},
  annote =	{Keywords: Galois theory, Coq, Mathematical Components, Dependent Type Theory, Abel-Ruffini, General quintic}
}
Document
Invited Talk
Mathematical Structures in Dependent Type Theory (Invited Talk)

Authors: Assia Mahboubi

Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)


Abstract
In this talk, we discuss the role and the implementation of mathematical structures in libraries of formalised mathematics in dependent type theory.

Cite as

Assia Mahboubi. Mathematical Structures in Dependent Type Theory (Invited Talk). In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 2:1-2:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{mahboubi:LIPIcs.CSL.2021.2,
  author =	{Mahboubi, Assia},
  title =	{{Mathematical Structures in Dependent Type Theory}},
  booktitle =	{29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
  pages =	{2:1--2:3},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-175-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{183},
  editor =	{Baier, Christel and Goubault-Larrecq, Jean},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.2},
  URN =		{urn:nbn:de:0030-drops-134361},
  doi =		{10.4230/LIPIcs.CSL.2021.2},
  annote =	{Keywords: Mathematical structures, formalized mathematics, dependent type theory}
}
Document
Complete Volume
LIPIcs, Volume 175, TYPES 2019, Complete Volume

Authors: Marc Bezem and Assia Mahboubi

Published in: LIPIcs, Volume 175, 25th International Conference on Types for Proofs and Programs (TYPES 2019)


Abstract
LIPIcs, Volume 175, TYPES 2019, Complete Volume

Cite as

25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 1-256, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@Proceedings{bezem_et_al:LIPIcs.TYPES.2019,
  title =	{{LIPIcs, Volume 175, TYPES 2019, Complete Volume}},
  booktitle =	{25th International Conference on Types for Proofs and Programs (TYPES 2019)},
  pages =	{1--256},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-158-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{175},
  editor =	{Bezem, Marc and Mahboubi, Assia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019},
  URN =		{urn:nbn:de:0030-drops-130639},
  doi =		{10.4230/LIPIcs.TYPES.2019},
  annote =	{Keywords: LIPIcs, Volume 175, TYPES 2019, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Marc Bezem and Assia Mahboubi

Published in: LIPIcs, Volume 175, 25th International Conference on Types for Proofs and Programs (TYPES 2019)


Abstract
Front Matter, Table of Contents, Preface, Conference Organization

Cite as

25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 0:i-0:x, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{bezem_et_al:LIPIcs.TYPES.2019.0,
  author =	{Bezem, Marc and Mahboubi, Assia},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{25th International Conference on Types for Proofs and Programs (TYPES 2019)},
  pages =	{0:i--0:x},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-158-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{175},
  editor =	{Bezem, Marc and Mahboubi, Assia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.0},
  URN =		{urn:nbn:de:0030-drops-130640},
  doi =		{10.4230/LIPIcs.TYPES.2019.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Making Isabelle Content Accessible in Knowledge Representation Formats

Authors: Michael Kohlhase, Florian Rabe, and Makarius Wenzel

Published in: LIPIcs, Volume 175, 25th International Conference on Types for Proofs and Programs (TYPES 2019)


Abstract
The libraries of proof assistants like Isabelle, Coq, HOL are notoriously difficult to interpret by external tools: de facto, only the prover itself can parse and process them adequately. In the case of Isabelle, an export of the library into a FAIR (Findable, Accessible, Interoperable, and Reusable) knowledge exchange format was already envisioned by the authors in 1999 but had previously proved too difficult. After substantial improvements of the Isabelle Prover IDE (PIDE) and the OMDoc/Mmt format since then, we are now able to deliver such an export. Concretely we present an integration of PIDE and Mmt that allows exporting all Isabelle libraries in OMDoc format. Our export covers the full Isabelle distribution and the Archive of Formal Proofs (AFP) - more than 12 thousand theories and locales resulting in over 65 GB of OMDoc/XML. Such a systematic export of Isabelle content to a well-defined interchange format like OMDoc enables many applications such as dependency management, independent proof checking, or library search.

Cite as

Michael Kohlhase, Florian Rabe, and Makarius Wenzel. Making Isabelle Content Accessible in Knowledge Representation Formats. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 1:1-1:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{kohlhase_et_al:LIPIcs.TYPES.2019.1,
  author =	{Kohlhase, Michael and Rabe, Florian and Wenzel, Makarius},
  title =	{{Making Isabelle Content Accessible in Knowledge Representation Formats}},
  booktitle =	{25th International Conference on Types for Proofs and Programs (TYPES 2019)},
  pages =	{1:1--1:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-158-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{175},
  editor =	{Bezem, Marc and Mahboubi, Assia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.1},
  URN =		{urn:nbn:de:0030-drops-130651},
  doi =		{10.4230/LIPIcs.TYPES.2019.1},
  annote =	{Keywords: Isabelle, PIDE, OMDoc, MMT, library, export}
}
Document
Type Theory Unchained: Extending Agda with User-Defined Rewrite Rules

Authors: Jesper Cockx

Published in: LIPIcs, Volume 175, 25th International Conference on Types for Proofs and Programs (TYPES 2019)


Abstract
Dependently typed languages such as Coq and Agda can statically guarantee the correctness of our proofs and programs. To provide this guarantee, they restrict users to certain schemes - such as strictly positive datatypes, complete case analysis, and well-founded induction - that are known to be safe. However, these restrictions can be too strict, making programs and proofs harder to write than necessary. On a higher level, they also prevent us from imagining the different ways the language could be extended. In this paper I show how to extend a dependently typed language with user-defined higher-order non-linear rewrite rules. Rewrite rules are a form of equality reflection that is applied automatically by the typechecker. I have implemented rewrite rules as an extension to Agda, and I give six examples how to use them both to make proofs easier and to experiment with extensions of type theory. I also show how to make rewrite rules interact well with other features of Agda such as η-equality, implicit arguments, data and record types, irrelevance, and universe level polymorphism. Thus rewrite rules break the chains on computation and put its power back into the hands of its rightful owner: yours.

Cite as

Jesper Cockx. Type Theory Unchained: Extending Agda with User-Defined Rewrite Rules. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 2:1-2:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{cockx:LIPIcs.TYPES.2019.2,
  author =	{Cockx, Jesper},
  title =	{{Type Theory Unchained: Extending Agda with User-Defined Rewrite Rules}},
  booktitle =	{25th International Conference on Types for Proofs and Programs (TYPES 2019)},
  pages =	{2:1--2:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-158-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{175},
  editor =	{Bezem, Marc and Mahboubi, Assia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.2},
  URN =		{urn:nbn:de:0030-drops-130666},
  doi =		{10.4230/LIPIcs.TYPES.2019.2},
  annote =	{Keywords: Dependent types, Proof assistants, Rewrite rules, Higher-order rewriting, Agda}
}
Document
A Quantitative Understanding of Pattern Matching

Authors: Sandra Alves, Delia Kesner, and Daniel Ventura

Published in: LIPIcs, Volume 175, 25th International Conference on Types for Proofs and Programs (TYPES 2019)


Abstract
This paper shows that the recent approach to quantitative typing systems for programming languages can be extended to pattern matching features. Indeed, we define two resource-aware type systems, named U and E, for a λ-calculus equipped with pairs for both patterns and terms. Our typing systems borrow some basic ideas from [Antonio Bucciarelli et al., 2015], which characterises (head) normalisation in a qualitative way, in the sense that typability and normalisation coincide. But, in contrast to [Antonio Bucciarelli et al., 2015], our systems also provide quantitative information about the dynamics of the calculus. Indeed, system U provides upper bounds for the length of (head) normalisation sequences plus the size of their corresponding normal forms, while system E, which can be seen as a refinement of system U, produces exact bounds for each of them. This is achieved by means of a non-idempotent intersection type system equipped with different technical tools. First of all, we use product types to type pairs instead of the disjoint unions in [Antonio Bucciarelli et al., 2015], which turn out to be an essential quantitative tool because they remove the confusion between "being a pair" and "being duplicable". Secondly, typing sequents in system E are decorated with tuples of integers, which provide quantitative information about normalisation sequences, notably time (cf. length) and space (cf. size). Moreover, the time resource information is remarkably refined, because it discriminates between different kinds of reduction steps performed during evaluation, so that beta, substitution and matching steps are counted separately. Another key tool of system E is that the type system distinguishes between consuming (contributing to time) and persistent (contributing to space) constructors.

Cite as

Sandra Alves, Delia Kesner, and Daniel Ventura. A Quantitative Understanding of Pattern Matching. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 3:1-3:36, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{alves_et_al:LIPIcs.TYPES.2019.3,
  author =	{Alves, Sandra and Kesner, Delia and Ventura, Daniel},
  title =	{{A Quantitative Understanding of Pattern Matching}},
  booktitle =	{25th International Conference on Types for Proofs and Programs (TYPES 2019)},
  pages =	{3:1--3:36},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-158-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{175},
  editor =	{Bezem, Marc and Mahboubi, Assia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.3},
  URN =		{urn:nbn:de:0030-drops-130672},
  doi =		{10.4230/LIPIcs.TYPES.2019.3},
  annote =	{Keywords: Intersection Types, Pattern Matching, Exact Bounds}
}
Document
Big Step Normalisation for Type Theory

Authors: Thorsten Altenkirch and Colin Geniet

Published in: LIPIcs, Volume 175, 25th International Conference on Types for Proofs and Programs (TYPES 2019)


Abstract
Big step normalisation is a normalisation method for typed lambda-calculi which relies on a purely syntactic recursive evaluator. Termination of that evaluator is proven using a predicate called strong computability, similar to the techniques used to prove strong normalisation of β-reduction for typed lambda-calculi. We generalise big step normalisation to a minimalist dependent type theory. Compared to previous presentations of big step normalisation for e.g. the simply-typed lambda-calculus, we use a quotiented syntax of type theory, which crucially reduces the syntactic complexity introduced by dependent types. Most of the proof has been formalised using Agda.

Cite as

Thorsten Altenkirch and Colin Geniet. Big Step Normalisation for Type Theory. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 4:1-4:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{altenkirch_et_al:LIPIcs.TYPES.2019.4,
  author =	{Altenkirch, Thorsten and Geniet, Colin},
  title =	{{Big Step Normalisation for Type Theory}},
  booktitle =	{25th International Conference on Types for Proofs and Programs (TYPES 2019)},
  pages =	{4:1--4:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-158-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{175},
  editor =	{Bezem, Marc and Mahboubi, Assia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.4},
  URN =		{urn:nbn:de:0030-drops-130682},
  doi =		{10.4230/LIPIcs.TYPES.2019.4},
  annote =	{Keywords: Normalisation, big step normalisation, type theory, dependent types, Agda}
}
  • Refine by Author
  • 10 Mahboubi, Assia
  • 2 Bezem, Marc
  • 2 Cohen, Cyril
  • 2 Sakaguchi, Kazuhiko
  • 1 Altenkirch, Thorsten
  • Show More...

  • Refine by Classification
  • 18 Theory of computation → Type theory
  • 5 Theory of computation → Logic and verification
  • 3 Theory of computation → Constructive mathematics
  • 2 Computing methodologies → Theorem proving algorithms
  • 2 Software and its engineering → Functional languages
  • Show More...

  • Refine by Keyword
  • 6 Coq
  • 3 type theory
  • 2 Agda
  • 2 Dependent types
  • 2 Elpi
  • Show More...

  • Refine by Type
  • 24 document
  • 1 volume

  • Refine by Publication Year
  • 14 2020
  • 3 2022
  • 2 2019
  • 2 2021
  • 2 2024
  • Show More...

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