20 Search Results for "Dybjer, Peter"

Volume

LIPIcs, Volume 130

24th International Conference on Types for Proofs and Programs (TYPES 2018)

TYPES 2018, June 18-21, 2018, Braga, Portugal

Editors: Peter Dybjer, José Espírito Santo, and Luís Pinto

Document
DOI: 10.4230/LIPIcs.ITP.2025.14
Canonical for Automated Theorem Proving in Lean

Authors: Chase Norman and Jeremy Avigad

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Canonical is a solver for type inhabitation in dependent type theory, that is, the problem of producing a term of a given type. We present a Lean tactic which invokes Canonical to generate proof terms and synthesize programs. The tactic supports higher-order and dependently-typed goals, structural recursion over indexed inductive types, and definitional equality. Canonical finds proofs for 84% of Natural Number Game problems in 51 seconds total.
Cite as

Chase Norman and Jeremy Avigad. Canonical for Automated Theorem Proving in Lean. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 14:1-14:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{norman_et_al:LIPIcs.ITP.2025.14,
  author =	{Norman, Chase and Avigad, Jeremy},
  title =	{{Canonical for Automated Theorem Proving in Lean}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{14:1--14:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.14},
  URN =		{urn:nbn:de:0030-drops-246128},
  doi =		{10.4230/LIPIcs.ITP.2025.14},
  annote =	{Keywords: Automated Reasoning, Interactive Theorem Proving, Dependent Type Theory, Inhabitation, Unification, Program Synthesis, Formal Methods}
}
Document
DOI: 10.4230/LIPIcs.CP.2025.40
An Efficient and Uniform CSP Solution Generator Generator

Authors: Ghiles Ziat and Martin Pépin

Published in: LIPIcs, Volume 340, 31st International Conference on Principles and Practice of Constraint Programming (CP 2025)

Abstract
Constraint-based random testing is a powerful technique which aims at generating random test cases to verify functional properties of a program. Its objective is to determine whether a function satisfies a given property for every possible input. This approach requires firstly defining the property to satisfy, then secondly to provide a "generator of inputs" able to feed the program with the inputs generated. Besides, function inputs often need to satisfy certain constraints to ensure the function operates correctly, which makes the crafting of such a generator a hard task. In this paper, we are interested in the problem of manufacturing a uniform and efficient generator for the solutions of a CSP. In order to do that, we propose a specialized solving method that produces a well-suited representation for random sampling. Our solving method employs a dedicated propagation scheme based on the hypergraph representation of a CSP, and a custom split heuristic called birdge-first that emphasizes the interests of our propagation scheme. The generators we build are general enough to handle a wide range of use-cases. They are moreover uniform by construction, iterative and self-improving. We present a prototype built upon the AbSolute constraint solving library and demonstrate its performances on several realistic examples.
Cite as

Ghiles Ziat and Martin Pépin. An Efficient and Uniform CSP Solution Generator Generator. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 40:1-40:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ziat_et_al:LIPIcs.CP.2025.40,
  author =	{Ziat, Ghiles and P\'{e}pin, Martin},
  title =	{{An Efficient and Uniform CSP Solution Generator Generator}},
  booktitle =	{31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
  pages =	{40:1--40:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-380-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{340},
  editor =	{de la Banda, Maria Garcia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.40},
  URN =		{urn:nbn:de:0030-drops-239010},
  doi =		{10.4230/LIPIcs.CP.2025.40},
  annote =	{Keywords: Constraint Programming, Property-based Testing}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSCD.2025.1
Computation First: Rebuilding Constructivism with Effects (Invited Talk)

Authors: Liron Cohen

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

Abstract
Constructive logic and type theory have traditionally been grounded in pure, effect-free model of computation. This paper argues that such a restriction is not a foundational necessity but a historical artifact, and it advocates for a broader perspective of effectful constructivism, where computational effects, such as state, non-determinism, and exceptions, are directly and internally embedded in the logical and computational foundations. We begin by surveying examples where effects reshape logical principles, and then outline three approaches to effectful constructivism, focusing on realizability models: Monadic Combinatory Algebras, which extend classical partial combinatory algebras with effectful computation; Evidenced Frames, a flexible semantic structure capable of uniformly capturing a wide range of effects; and Effectful Higher-Order Logic (EffHOL), a syntactic approach that directly translates logical propositions into specifications for effectful programs. We further illustrate how concrete type theories can internalize effects, via the family of type theories TT^□_C. Together, these works demonstrate that effectful constructivism is not merely possible but a natural and robust extension of traditional frameworks.
Cite as

Liron Cohen. Computation First: Rebuilding Constructivism with Effects (Invited Talk). In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 1:1-1:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{cohen:LIPIcs.FSCD.2025.1,
  author =	{Cohen, Liron},
  title =	{{Computation First: Rebuilding Constructivism with Effects}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{1:1--1:20},
  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.1},
  URN =		{urn:nbn:de:0030-drops-236167},
  doi =		{10.4230/LIPIcs.FSCD.2025.1},
  annote =	{Keywords: Effectful constructivism, realizability, type theory, monadic combinatory algebras, evidenced frame}
}
Document
DOI: 10.4230/LIPIcs.STACS.2025.40
Identity-Preserving Lax Extensions and Where to Find Them

Authors: Sergey Goncharov, Dirk Hofmann, Pedro Nora, Lutz Schröder, and Paul Wild

Published in: LIPIcs, Volume 327, 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)

Abstract
Generic notions of bisimulation for various types of systems (nondeterministic, probabilistic, weighted etc.) rely on identity-preserving (normal) lax extensions of the functor encapsulating the system type, in the paradigm of universal coalgebra. It is known that preservation of weak pullbacks is a sufficient condition for a functor to admit a normal lax extension (the Barr extension, which in fact is then even strict); in the converse direction, nothing is currently known about necessary (weak) pullback preservation conditions for the existence of normal lax extensions. In the present work, we narrow this gap by showing on the one hand that functors admitting a normal lax extension preserve 1/4-iso pullbacks, i.e. pullbacks in which at least one of the projections is an isomorphism. On the other hand, we give sufficient conditions, showing that a functor admits a normal lax extension if it weakly preserves either 1/4-iso pullbacks and 4/4-epi pullbacks (i.e. pullbacks in which all morphisms are epic) or inverse images. We apply these criteria to concrete examples, in particular to functors modelling neighbourhood systems and weighted systems.
Cite as

Sergey Goncharov, Dirk Hofmann, Pedro Nora, Lutz Schröder, and Paul Wild. Identity-Preserving Lax Extensions and Where to Find Them. In 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 327, pp. 40:1-40:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{goncharov_et_al:LIPIcs.STACS.2025.40,
  author =	{Goncharov, Sergey and Hofmann, Dirk and Nora, Pedro and Schr\"{o}der, Lutz and Wild, Paul},
  title =	{{Identity-Preserving Lax Extensions and Where to Find Them}},
  booktitle =	{42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)},
  pages =	{40:1--40:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-365-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{327},
  editor =	{Beyersdorff, Olaf and Pilipczuk, Micha{\l} and Pimentel, Elaine and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2025.40},
  URN =		{urn:nbn:de:0030-drops-228665},
  doi =		{10.4230/LIPIcs.STACS.2025.40},
  annote =	{Keywords: (Bi-)simulations, lax extensions, modal logics, coalgebra}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2024.4
AMECOS: A Modular Event-Based Framework for Concurrent Object Specification

Authors: Timothé Albouy, Antonio Fernández Anta, Chryssis Georgiou, Mathieu Gestin, Nicolas Nicolaou, and Junlang Wang

Published in: LIPIcs, Volume 324, 28th International Conference on Principles of Distributed Systems (OPODIS 2024)

Abstract
In this work, we introduce a modular framework for specifying distributed systems that we call AMECOS. Specifically, our framework departs from the traditional use of sequential specification, which presents limitations both on the specification expressiveness and implementation efficiency of inherently concurrent objects, as documented by Castañeda, Rajsbaum and Raynal in CACM 2023. Our framework focuses on the interactions between the various system components, specified as concurrent objects. Interactions are described with sequences of object events. This provides a modular way of specifying distributed systems and separates legality (object semantics) from other issues, such as consistency. We demonstrate the usability of our framework by (i) specifying various well-known concurrent objects, such as registers, shared memory, message-passing, reliable broadcast, and consensus, (ii) providing hierarchies of ordering semantics (namely, consistency hierarchy, memory hierarchy, and reliable broadcast hierarchy), and (iii) presenting a novel axiomatic proof of the impossibility of the well-known Consensus problem.
Cite as

Timothé Albouy, Antonio Fernández Anta, Chryssis Georgiou, Mathieu Gestin, Nicolas Nicolaou, and Junlang Wang. AMECOS: A Modular Event-Based Framework for Concurrent Object Specification. In 28th International Conference on Principles of Distributed Systems (OPODIS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 324, pp. 4:1-4:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{albouy_et_al:LIPIcs.OPODIS.2024.4,
  author =	{Albouy, Timoth\'{e} and Fern\'{a}ndez Anta, Antonio and Georgiou, Chryssis and Gestin, Mathieu and Nicolaou, Nicolas and Wang, Junlang},
  title =	{{AMECOS: A Modular Event-Based Framework for Concurrent Object Specification}},
  booktitle =	{28th International Conference on Principles of Distributed Systems (OPODIS 2024)},
  pages =	{4:1--4:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-360-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{324},
  editor =	{Bonomi, Silvia and Galletta, Letterio and Rivi\`{e}re, Etienne and Schiavoni, Valerio},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2024.4},
  URN =		{urn:nbn:de:0030-drops-225409},
  doi =		{10.4230/LIPIcs.OPODIS.2024.4},
  annote =	{Keywords: Concurrency, Object specification, Consistency conditions, Consensus impossibility}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2022.13
Type Theory with Explicit Universe Polymorphism

Authors: Marc Bezem, Thierry Coquand, Peter Dybjer, and Martín Escardó

Published in: LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)

Abstract
The aim of this paper is to refine and extend proposals by Sozeau and Tabareau and by Voevodsky for universe polymorphism in type theory. In those systems judgments can depend on explicit constraints between universe levels. We here present a system where we also have products indexed by universe levels and by constraints. Our theory has judgments for internal universe levels, built up from level variables by a successor operation and a binary supremum operation, and also judgments for equality of universe levels.
Cite as

Marc Bezem, Thierry Coquand, Peter Dybjer, and Martín Escardó. Type Theory with Explicit Universe Polymorphism. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 13:1-13:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{bezem_et_al:LIPIcs.TYPES.2022.13,
  author =	{Bezem, Marc and Coquand, Thierry and Dybjer, Peter and Escard\'{o}, Mart{\'\i}n},
  title =	{{Type Theory with Explicit Universe Polymorphism}},
  booktitle =	{28th International Conference on Types for Proofs and Programs (TYPES 2022)},
  pages =	{13:1--13:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-285-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{269},
  editor =	{Kesner, Delia and P\'{e}drot, Pierre-Marie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.13},
  URN =		{urn:nbn:de:0030-drops-184564},
  doi =		{10.4230/LIPIcs.TYPES.2022.13},
  annote =	{Keywords: type theory, universes in type theory, universe polymorphism, level-indexed products, constraint-indexed products}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2022.14
A Univalent Formalization of Constructive Affine Schemes

Authors: Max Zeuner and Anders Mörtberg

Published in: LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)

Abstract
We present a formalization of constructive affine schemes in the Cubical Agda proof assistant. This development is not only fully constructive and predicative, it also makes crucial use of univalence. By now schemes have been formalized in various proof assistants. However, most existing formalizations follow the inherently non-constructive approach of Hartshorne’s classic "Algebraic Geometry" textbook, for which the construction of the so-called structure sheaf is rather straightforwardly formalizable and works the same with or without univalence. We follow an alternative approach that uses a point-free description of the constructive counterpart of the Zariski spectrum called the Zariski lattice and proceeds by defining the structure sheaf on formal basic opens and then lift it to the whole lattice. This general strategy is used in a plethora of textbooks, but formalizing it has proved tricky. The main result of this paper is that with the help of the univalence principle we can make this "lift from basis" strategy formal and obtain a fully formalized account of constructive affine schemes.
Cite as

Max Zeuner and Anders Mörtberg. A Univalent Formalization of Constructive Affine Schemes. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 14:1-14:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{zeuner_et_al:LIPIcs.TYPES.2022.14,
  author =	{Zeuner, Max and M\"{o}rtberg, Anders},
  title =	{{A Univalent Formalization of Constructive Affine Schemes}},
  booktitle =	{28th International Conference on Types for Proofs and Programs (TYPES 2022)},
  pages =	{14:1--14:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-285-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{269},
  editor =	{Kesner, Delia and P\'{e}drot, Pierre-Marie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.14},
  URN =		{urn:nbn:de:0030-drops-184574},
  doi =		{10.4230/LIPIcs.TYPES.2022.14},
  annote =	{Keywords: Affine Schemes, Homotopy Type Theory and Univalent Foundations, Cubical Agda, Constructive Mathematics}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2019.8
Coherence for Monoidal Groupoids in HoTT

Authors: Stefano Piceghello

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

Abstract
We present a proof of coherence for monoidal groupoids in homotopy type theory. An important role in the formulation and in the proof of coherence is played by groupoids with a free monoidal structure; these can be represented by 1-truncated higher inductive types, with constructors freely generating their defining objects, natural isomorphisms and commutative diagrams. All results included in this paper have been formalised in the proof assistant Coq.
Cite as

Stefano Piceghello. Coherence for Monoidal Groupoids in HoTT. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 8:1-8:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{piceghello:LIPIcs.TYPES.2019.8,
  author =	{Piceghello, Stefano},
  title =	{{Coherence for Monoidal Groupoids in HoTT}},
  booktitle =	{25th International Conference on Types for Proofs and Programs (TYPES 2019)},
  pages =	{8:1--8: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.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.8},
  URN =		{urn:nbn:de:0030-drops-130722},
  doi =		{10.4230/LIPIcs.TYPES.2019.8},
  annote =	{Keywords: homotopy type theory, coherence, monoidal categories, groupoids, higher inductive types, formalisation, Coq}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.TYPES.2018
LIPIcs, Volume 130, TYPES'18, Complete Volume

Authors: Peter Dybjer, José Espírito Santo, and Luís Pinto

Published in: LIPIcs, Volume 130, 24th International Conference on Types for Proofs and Programs (TYPES 2018)

Abstract
LIPIcs, Volume 130, TYPES'18, Complete Volume
Cite as

24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@Proceedings{dybjer_et_al:LIPIcs.TYPES.2018,
  title =	{{LIPIcs, Volume 130, TYPES'18, Complete Volume}},
  booktitle =	{24th International Conference on Types for Proofs and Programs (TYPES 2018)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-106-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{130},
  editor =	{Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018},
  URN =		{urn:nbn:de:0030-drops-114507},
  doi =		{10.4230/LIPIcs.TYPES.2018},
  annote =	{Keywords: Theory of computation,Type theory; Constructive mathematics; Logic and verification; Program verification, Software and its engineering}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.TYPES.2018.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Peter Dybjer, José Espírito Santo, and Luís Pinto

Published in: LIPIcs, Volume 130, 24th International Conference on Types for Proofs and Programs (TYPES 2018)

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

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

Copy BibTex To Clipboard

@InProceedings{dybjer_et_al:LIPIcs.TYPES.2018.0,
  author =	{Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{24th International Conference on Types for Proofs and Programs (TYPES 2018)},
  pages =	{0:i--0:x},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-106-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{130},
  editor =	{Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.0},
  URN =		{urn:nbn:de:0030-drops-114045},
  doi =		{10.4230/LIPIcs.TYPES.2018.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2018.1
Martin Hofmann’s Case for Non-Strictly Positive Data Types

Authors: Ulrich Berger, Ralph Matthes, and Anton Setzer

Published in: LIPIcs, Volume 130, 24th International Conference on Types for Proofs and Programs (TYPES 2018)

Abstract
We describe the breadth-first traversal algorithm by Martin Hofmann that uses a non-strictly positive data type and carry out a simple verification in an extensional setting. Termination is shown by implementing the algorithm in the strongly normalising extension of system F by Mendler-style recursion. We then analyze the same algorithm by alternative verifications first in an intensional setting using a non-strictly positive inductive definition (not just a non-strictly positive data type), and subsequently by two different algebraic reductions. The verification approaches are compared in terms of notions of simulation and should elucidate the somewhat mysterious algorithm and thus make a case for other uses of non-strictly positive data types. Except for the termination proof, which cannot be formalised in Coq, all proofs were formalised in Coq and some of the algorithms were implemented in Agda and Haskell.
Cite as

Ulrich Berger, Ralph Matthes, and Anton Setzer. Martin Hofmann’s Case for Non-Strictly Positive Data Types. In 24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, pp. 1:1-1:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{berger_et_al:LIPIcs.TYPES.2018.1,
  author =	{Berger, Ulrich and Matthes, Ralph and Setzer, Anton},
  title =	{{Martin Hofmann’s Case for Non-Strictly Positive Data Types}},
  booktitle =	{24th International Conference on Types for Proofs and Programs (TYPES 2018)},
  pages =	{1:1--1:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-106-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{130},
  editor =	{Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.1},
  URN =		{urn:nbn:de:0030-drops-114052},
  doi =		{10.4230/LIPIcs.TYPES.2018.1},
  annote =	{Keywords: non strictly-positive data types, breadth-first traversal, program verification, Mendler-style recursion, System F, theorem proving, Coq, Agda, Haskell}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2018.2
A Simpler Undecidability Proof for System F Inhabitation

Authors: Andrej Dudenhefner and Jakob Rehof

Published in: LIPIcs, Volume 130, 24th International Conference on Types for Proofs and Programs (TYPES 2018)

Abstract
Provability in the intuitionistic second-order propositional logic (resp. inhabitation in the polymorphic lambda-calculus) was shown by Löb to be undecidable in 1976. Since the original proof is heavily condensed, Arts in collaboration with Dekkers provided a fully unfolded argument in 1992 spanning approximately fifty pages. Later in 1997, Urzyczyn developed a different, syntax oriented proof. Each of the above approaches embeds (an undecidable fragment of) first-order predicate logic into second-order propositional logic. In this work, we develop a simpler undecidability proof by reduction from solvability of Diophantine equations (is there an integer solution to P(x_1, ..., x_n) = 0 where P is a polynomial with integer coefficients?). Compared to the previous approaches, the given reduction is more accessible for formalization and more comprehensible for didactic purposes. Additionally, we formalize soundness and completeness of the reduction in the Coq proof assistant under the banner of "type theory inside type theory".
Cite as

Andrej Dudenhefner and Jakob Rehof. A Simpler Undecidability Proof for System F Inhabitation. In 24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, pp. 2:1-2:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{dudenhefner_et_al:LIPIcs.TYPES.2018.2,
  author =	{Dudenhefner, Andrej and Rehof, Jakob},
  title =	{{A Simpler Undecidability Proof for System F Inhabitation}},
  booktitle =	{24th International Conference on Types for Proofs and Programs (TYPES 2018)},
  pages =	{2:1--2:11},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-106-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{130},
  editor =	{Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.2},
  URN =		{urn:nbn:de:0030-drops-114061},
  doi =		{10.4230/LIPIcs.TYPES.2018.2},
  annote =	{Keywords: System F, Lambda Calculus, Inhabitation, Propositional Logic, Provability, Undecidability, Coq, Formalization}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2018.3
Dependent Sums and Dependent Products in Bishop’s Set Theory

Authors: Iosif Petrakis

Published in: LIPIcs, Volume 130, 24th International Conference on Types for Proofs and Programs (TYPES 2018)

Abstract
According to the standard, non type-theoretic accounts of Bishop’s constructivism (BISH), dependent functions are not necessary to BISH. Dependent functions though, are explicitly used by Bishop in his definition of the intersection of a family of subsets, and they are necessary to the definition of arbitrary products. In this paper we present the basic notions and principles of CSFT, a semi-formal constructive theory of sets and functions intended to be a minimal, adequate and faithful, in Feferman’s sense, semi-formalisation of Bishop’s set theory (BST). We define the notions of dependent sum (or exterior union) and dependent product of set-indexed families of sets within CSFT, and we prove the distributivity of prod over sum i.e., the translation of the type-theoretic axiom of choice within CSFT. We also define the notions of dependent sum (or interior union) and dependent product of set-indexed families of subsets within CSFT. For these definitions we extend BST with the universe of sets #1 V_0 and the universe of functions #1 V_1.
Cite as

Iosif Petrakis. Dependent Sums and Dependent Products in Bishop’s Set Theory. In 24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, pp. 3:1-3:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{petrakis:LIPIcs.TYPES.2018.3,
  author =	{Petrakis, Iosif},
  title =	{{Dependent Sums and Dependent Products in Bishop’s Set Theory}},
  booktitle =	{24th International Conference on Types for Proofs and Programs (TYPES 2018)},
  pages =	{3:1--3:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-106-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{130},
  editor =	{Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.3},
  URN =		{urn:nbn:de:0030-drops-114070},
  doi =		{10.4230/LIPIcs.TYPES.2018.3},
  annote =	{Keywords: Bishop’s constructive mathematics, Martin-L\"{o}f’s type theory, dependent sums, dependent products, type-theoretic axiom of choice}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2018.4
Semantic Subtyping for Non-Strict Languages

Authors: Tommaso Petrucciani, Giuseppe Castagna, Davide Ancona, and Elena Zucca

Published in: LIPIcs, Volume 130, 24th International Conference on Types for Proofs and Programs (TYPES 2018)

Abstract
Semantic subtyping is an approach to define subtyping relations for type systems featuring union and intersection type connectives. It has been studied only for strict languages, and it is unsound for non-strict semantics. In this work, we study how to adapt this approach to non-strict languages: in particular, we define a type system using semantic subtyping for a functional language with a call-by-need semantics. We do so by introducing an explicit representation for divergence in the types, so that the type system distinguishes expressions that are results from those which are computations that might diverge.
Cite as

Tommaso Petrucciani, Giuseppe Castagna, Davide Ancona, and Elena Zucca. Semantic Subtyping for Non-Strict Languages. In 24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, pp. 4:1-4:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{petrucciani_et_al:LIPIcs.TYPES.2018.4,
  author =	{Petrucciani, Tommaso and Castagna, Giuseppe and Ancona, Davide and Zucca, Elena},
  title =	{{Semantic Subtyping for Non-Strict Languages}},
  booktitle =	{24th International Conference on Types for Proofs and Programs (TYPES 2018)},
  pages =	{4:1--4:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-106-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{130},
  editor =	{Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.4},
  URN =		{urn:nbn:de:0030-drops-114083},
  doi =		{10.4230/LIPIcs.TYPES.2018.4},
  annote =	{Keywords: Semantic subtyping, non-strict semantics, call-by-need, union types, intersection types}
}
  • Refine by Type
  • 19 Document/PDF
  • 5 Document/HTML
  • 1 Volume

  • Refine by Publication Year
  • 5 2025
  • 2 2023
  • 1 2020
  • 10 2019
  • 1 2015
  • Show More...

  • Refine by Author
  • 5 Dybjer, Peter
  • 2 Espírito Santo, José
  • 2 Pinto, Luís
  • 1 Albouy, Timothé
  • 1 Ancona, Davide
  • Show More...

  • Refine by Series/Journal
  • 18 LIPIcs
  • 1 DagSemRep

  • Refine by Classification
  • 9 Theory of computation → Type theory
  • 5 Theory of computation → Constructive mathematics
  • 5 Theory of computation → Logic and verification
  • 3 Software and its engineering → Functional languages
  • 2 Theory of computation → Program verification
  • Show More...

  • Refine by Keyword
  • 3 Coq
  • 2 Agda
  • 2 Formalization
  • 2 Inhabitation
  • 2 System F
  • 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact