16 Search Results for "Abel, Andreas"

Volume

LIPIcs, Volume 104

23rd International Conference on Types for Proofs and Programs (TYPES 2017)

TYPES 2017, May 29 to June 1, 2017, Budapest, Hungary

Editors: Andreas Abel, Fredrik Nordvall Forsberg, and Ambrus Kaposi

Document
DOI: 10.4230/LIPIcs.ITP.2021.13
Flexible Coinduction in Agda

Authors: Luca Ciccone, Francesco Dagnino, and Elena Zucca

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

Abstract
We provide an Agda library for inference systems, also supporting their recent generalization allowing flexible coinduction, that is, interpretations which are neither inductive, nor purely coinductive. A specific inference system can be obtained as an instance by writing a set of meta-rules, in an Agda format which closely resembles the usual one. In this way, the user gets for free the related properties, notably the inductive and coinductive intepretation and the corresponding proof principles. Moreover, a significant modularity is achieved. Indeed, rather than being defined from scratch and with a built-in interpretation, an inference system can also be obtained by composition operators, such as union and restriction to a smaller universe, and its semantics can be modularly chosen as well. In particular, flexible coinduction is obtained by composing in a certain way the interpretations of two inference systems. We illustrate the use of the library by several examples. The most significant one is a big-step semantics for the λ-calculus, where flexible coinduction allows to obtain a special result (∞) for all and only the diverging computations, and the proof of equivalence with small-step semantics is carried out by relying on the proof principles offered by the library.
Cite as

Luca Ciccone, Francesco Dagnino, and Elena Zucca. Flexible Coinduction in Agda. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 13:1-13:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{ciccone_et_al:LIPIcs.ITP.2021.13,
  author =	{Ciccone, Luca and Dagnino, Francesco and Zucca, Elena},
  title =	{{Flexible Coinduction in Agda}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{13:1--13:19},
  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.13},
  URN =		{urn:nbn:de:0030-drops-139083},
  doi =		{10.4230/LIPIcs.ITP.2021.13},
  annote =	{Keywords: inference systems, induction, coinduction}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2020.1
On Model-Theoretic Strong Normalization for Truth-Table Natural Deduction

Authors: Andreas Abel

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

Abstract
Intuitionistic truth table natural deduction (ITTND) by Geuvers and Hurkens (2017), which is inherently non-confluent, has been shown strongly normalizing (SN) using continuation-passing-style translations to parallel lambda calculus by Geuvers, van der Giessen, and Hurkens (2019). We investigate the applicability of standard model-theoretic proof techniques and show (1) SN of detour reduction (β) using Girard’s reducibility candidates, and (2) SN of detour and permutation reduction (βπ) using biorthogonals. In the appendix, we adapt Tait’s method of saturated sets to β, clarifying the original proof of 2017, and extend it to βπ.
Cite as

Andreas Abel. On Model-Theoretic Strong Normalization for Truth-Table Natural Deduction. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 1:1-1:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{abel:LIPIcs.TYPES.2020.1,
  author =	{Abel, Andreas},
  title =	{{On Model-Theoretic Strong Normalization for Truth-Table Natural Deduction}},
  booktitle =	{26th International Conference on Types for Proofs and Programs (TYPES 2020)},
  pages =	{1:1--1:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-182-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{188},
  editor =	{de'Liguoro, Ugo and Berardi, Stefano and Altenkirch, Thorsten},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.1},
  URN =		{urn:nbn:de:0030-drops-138805},
  doi =		{10.4230/LIPIcs.TYPES.2020.1},
  annote =	{Keywords: Natural deduction, Permutative conversion, Reducibility, Strong normalization, Truth table}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2020.31
Encoding Agda Programs Using Rewriting

Authors: Guillaume Genestier

Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)

Abstract
We present in this paper an encoding in an extension with rewriting of the Edimburgh Logical Framework (LF) [Harper et al., 1993] of two common features: universe polymorphism and eta-convertibility. This encoding is at the root of the translator between Agda and Dedukti developped by the author.
Cite as

Guillaume Genestier. Encoding Agda Programs Using Rewriting. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 31:1-31:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{genestier:LIPIcs.FSCD.2020.31,
  author =	{Genestier, Guillaume},
  title =	{{Encoding Agda Programs Using Rewriting}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{31:1--31:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Ariola, Zena M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.31},
  URN =		{urn:nbn:de:0030-drops-123530},
  doi =		{10.4230/LIPIcs.FSCD.2020.31},
  annote =	{Keywords: Logical Frameworks, Rewriting, Universe Polymorphism, Eta Conversion}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2018.6
Normalization by Evaluation for Typed Weak lambda-Reduction

Authors: Filippo Sestini

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

Abstract
Weak reduction relations in the lambda-calculus are characterized by the rejection of the so-called xi-rule, which allows arbitrary reductions under abstractions. A notable instance of weak reduction can be found in the literature under the name restricted reduction or weak lambda-reduction. In this work, we attack the problem of algorithmically computing normal forms for lambda-wk, the lambda-calculus with weak lambda-reduction. We do so by first contrasting it with other weak systems, arguing that their notion of reduction is not strong enough to compute lambda-wk-normal forms. We observe that some aspects of weak lambda-reduction prevent us from normalizing lambda-wk directly, thus devise a new, better-behaved weak calculus lambda-ex, and reduce the normalization problem for lambda-w to that of lambda-ex. We finally define type systems for both calculi and apply Normalization by Evaluation to lambda-ex, obtaining a normalization proof for lambda-wk as a corollary. We formalize all our results in Agda, a proof-assistant based on intensional Martin-Löf Type Theory.
Cite as

Filippo Sestini. Normalization by Evaluation for Typed Weak lambda-Reduction. In 24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, pp. 6:1-6:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{sestini:LIPIcs.TYPES.2018.6,
  author =	{Sestini, Filippo},
  title =	{{Normalization by Evaluation for Typed Weak lambda-Reduction}},
  booktitle =	{24th International Conference on Types for Proofs and Programs (TYPES 2018)},
  pages =	{6:1--6:17},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.6},
  URN =		{urn:nbn:de:0030-drops-114101},
  doi =		{10.4230/LIPIcs.TYPES.2018.6},
  annote =	{Keywords: normalization, lambda-calculus, reduction, term-rewriting, Agda}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2019.32
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
Complete Volume
DOI: 10.4230/LIPIcs.TYPES.2017
LIPIcs, Volume 104, TYPES'17, Complete Volume

Authors: Andreas Abel, Fredrik Nordvall Forsberg, and Ambrus Kaposi

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

Abstract
LIPIcs, Volume 104, TYPES'17, Complete Volume
Cite as

23rd International Conference on Types for Proofs and Programs (TYPES 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 104, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@Proceedings{abel_et_al:LIPIcs.TYPES.2017,
  title =	{{LIPIcs, Volume 104, TYPES'17, Complete Volume}},
  booktitle =	{23rd International Conference on Types for Proofs and Programs (TYPES 2017)},
  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},
  URN =		{urn:nbn:de:0030-drops-101671},
  doi =		{10.4230/LIPIcs.TYPES.2017},
  annote =	{Keywords: Theory of computation, Type theory, Proof theory, Program verification}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.TYPES.2017.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Andreas Abel, Fredrik Nordvall Forsberg, and Ambrus Kaposi

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

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

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

Copy BibTex To Clipboard

@InProceedings{abel_et_al:LIPIcs.TYPES.2017.0,
  author =	{Abel, Andreas and Nordvall Forsberg, Fredrik and Kaposi, Ambrus},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{23rd International Conference on Types for Proofs and Programs (TYPES 2017)},
  pages =	{0:i--0:x},
  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.0},
  URN =		{urn:nbn:de:0030-drops-100488},
  doi =		{10.4230/LIPIcs.TYPES.2017.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2017.1
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
DOI: 10.4230/LIPIcs.TYPES.2017.2
Lower End of the Linial-Post Spectrum

Authors: Andrej Dudenhefner and Jakob Rehof

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

Abstract
We show that recognizing axiomatizations of the Hilbert-style calculus containing only the axiom a -> (b -> a) is undecidable (a reduction from the Post correspondence problem is formalized in the Lean theorem prover). Interestingly, the problem remains undecidable considering only axioms which, when seen as simple types, are principal for some lambda-terms in beta-normal form. This problem is closely related to type-based composition synthesis, i.e. finding a composition of given building blocks (typed terms) satisfying a desired specification (goal type). Contrary to the above result, axiomatizations of the Hilbert-style calculus containing only the axiom a -> (b -> b) are recognizable in linear time.
Cite as

Andrej Dudenhefner and Jakob Rehof. Lower End of the Linial-Post Spectrum. In 23rd International Conference on Types for Proofs and Programs (TYPES 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 104, pp. 2:1-2:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{dudenhefner_et_al:LIPIcs.TYPES.2017.2,
  author =	{Dudenhefner, Andrej and Rehof, Jakob},
  title =	{{Lower End of the Linial-Post Spectrum}},
  booktitle =	{23rd International Conference on Types for Proofs and Programs (TYPES 2017)},
  pages =	{2:1--2:15},
  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.2},
  URN =		{urn:nbn:de:0030-drops-100503},
  doi =		{10.4230/LIPIcs.TYPES.2017.2},
  annote =	{Keywords: combinatory logic, lambda calculus, type theory, simple types, inhabitation, principal type}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2017.3
Proof Terms for Generalized Natural Deduction

Authors: Herman Geuvers and Tonny Hurkens

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

Abstract
In previous work it has been shown how to generate natural deduction rules for propositional connectives from truth tables, both for classical and constructive logic. The present paper extends this for the constructive case with proof-terms, thereby extending the Curry-Howard isomorphism to these new connectives. A general notion of conversion of proofs is defined, both as a conversion of derivations and as a reduction of proof-terms. It is shown how the well-known rules for natural deduction (Gentzen, Prawitz) and general elimination rules (Schroeder-Heister, von Plato, and others), and their proof conversions can be found as instances. As an illustration of the power of the method, we give constructive rules for the nand logical operator (also called Sheffer stroke). As usual, conversions come in two flavours: either a detour conversion arising from a detour convertibility, where an introduction rule is immediately followed by an elimination rule, or a permutation conversion arising from an permutation convertibility, an elimination rule nested inside another elimination rule. In this paper, both are defined for the general setting, as conversions of derivations and as reductions of proof-terms. The properties of these are studied as proof-term reductions. As one of the main contributions it is proved that detour conversion is strongly normalizing and permutation conversion is strongly normalizing: no matter how one reduces, the process eventually terminates. Furthermore, the combination of the two conversions is shown to be weakly normalizing: one can always reduce away all convertibilities.
Cite as

Herman Geuvers and Tonny Hurkens. Proof Terms for Generalized Natural Deduction. In 23rd International Conference on Types for Proofs and Programs (TYPES 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 104, pp. 3:1-3:39, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{geuvers_et_al:LIPIcs.TYPES.2017.3,
  author =	{Geuvers, Herman and Hurkens, Tonny},
  title =	{{Proof Terms for Generalized Natural Deduction}},
  booktitle =	{23rd International Conference on Types for Proofs and Programs (TYPES 2017)},
  pages =	{3:1--3:39},
  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.3},
  URN =		{urn:nbn:de:0030-drops-100519},
  doi =		{10.4230/LIPIcs.TYPES.2017.3},
  annote =	{Keywords: constructive logic, natural deduction, detour conversion, permutation conversion, normalization Curry-Howard isomorphism}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2017.4
PML2: Integrated Program Verification in ML

Authors: Rodolphe Lepigre

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

Abstract
We present the PML_2 language, which provides a uniform environment for programming, and for proving properties of programs in an ML-like setting. The language is Curry-style and call-by-value, it provides a control operator (interpreted in terms of classical logic), it supports general recursion and a very general form of (implicit, non-coercive) subtyping. In the system, equational properties of programs are expressed using two new type formers, and they are proved by constructing terminating programs. Although proofs rely heavily on equational reasoning, equalities are exclusively managed by the type-checker. This means that the user only has to choose which equality to use, and not where to use it, as is usually done in mathematical proofs. In the system, writing proofs mostly amounts to applying lemmas (possibly recursive function calls), and to perform case analyses (pattern matchings).
Cite as

Rodolphe Lepigre. PML2: Integrated Program Verification in ML. In 23rd International Conference on Types for Proofs and Programs (TYPES 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 104, pp. 4:1-4:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{lepigre:LIPIcs.TYPES.2017.4,
  author =	{Lepigre, Rodolphe},
  title =	{{PML2: Integrated Program Verification in ML}},
  booktitle =	{23rd International Conference on Types for Proofs and Programs (TYPES 2017)},
  pages =	{4:1--4:27},
  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.4},
  URN =		{urn:nbn:de:0030-drops-100521},
  doi =		{10.4230/LIPIcs.TYPES.2017.4},
  annote =	{Keywords: program verification, classical logic, ML-like language, termination checking, Curry-style quantification, implicit subtyping}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2017.5
Formalized Proof Systems for Propositional Logic

Authors: Julius Michaelis and Tobias Nipkow

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

Abstract
We have formalized a range of proof systems for classical propositional logic (sequent calculus, natural deduction, Hilbert systems, resolution) in Isabelle/HOL and have proved the most important meta-theoretic results about semantics and proofs: compactness, soundness, completeness, translations between proof systems, cut-elimination, interpolation and model existence.
Cite as

Julius Michaelis and Tobias Nipkow. Formalized Proof Systems for Propositional Logic. In 23rd International Conference on Types for Proofs and Programs (TYPES 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 104, pp. 5:1-5:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{michaelis_et_al:LIPIcs.TYPES.2017.5,
  author =	{Michaelis, Julius and Nipkow, Tobias},
  title =	{{Formalized Proof Systems for Propositional Logic}},
  booktitle =	{23rd International Conference on Types for Proofs and Programs (TYPES 2017)},
  pages =	{5:1--5:16},
  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.5},
  URN =		{urn:nbn:de:0030-drops-100537},
  doi =		{10.4230/LIPIcs.TYPES.2017.5},
  annote =	{Keywords: formalization of logic, proof systems, sequent calculus, natural deduction, resolution}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2017.6
Decomposing the Univalence Axiom

Authors: Ian Orton and Andrew M. Pitts

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

Abstract
This paper investigates Voevodsky's univalence axiom in intensional Martin-Löf type theory. In particular, it looks at how univalence can be derived from simpler axioms. We first present some existing work, collected together from various published and unpublished sources; we then present a new decomposition of the univalence axiom into simpler axioms. We argue that these axioms are easier to verify in certain potential models of univalent type theory, particularly those models based on cubical sets. Finally we show how this decomposition is relevant to an open problem in type theory.
Cite as

Ian Orton and Andrew M. Pitts. Decomposing the Univalence Axiom. In 23rd International Conference on Types for Proofs and Programs (TYPES 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 104, pp. 6:1-6:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{orton_et_al:LIPIcs.TYPES.2017.6,
  author =	{Orton, Ian and Pitts, Andrew M.},
  title =	{{Decomposing the Univalence Axiom}},
  booktitle =	{23rd International Conference on Types for Proofs and Programs (TYPES 2017)},
  pages =	{6:1--6:19},
  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.6},
  URN =		{urn:nbn:de:0030-drops-100546},
  doi =		{10.4230/LIPIcs.TYPES.2017.6},
  annote =	{Keywords: dependent type theory, homotopy type theory, univalent type theory, univalence, cubical type theory, cubical sets}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2017.7
On Equality of Objects in Categories in Constructive Type Theory

Authors: Erik Palmgren

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

Abstract
In this note we remark on the problem of equality of objects in categories formalized in Martin-Löf's constructive type theory. A standard notion of category in this system is E-category, where no such equality is specified. The main observation here is that there is no general extension of E-categories to categories with equality on objects, unless the principle Uniqueness of Identity Proofs (UIP) holds. We also introduce the notion of an H-category with equality on objects, which makes it easy to compare to the notion of univalent category proposed for Univalent Type Theory by Ahrens, Kapulkin and Shulman.
Cite as

Erik Palmgren. On Equality of Objects in Categories in Constructive Type Theory. In 23rd International Conference on Types for Proofs and Programs (TYPES 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 104, pp. 7:1-7:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{palmgren:LIPIcs.TYPES.2017.7,
  author =	{Palmgren, Erik},
  title =	{{On Equality of Objects in Categories in Constructive Type Theory}},
  booktitle =	{23rd International Conference on Types for Proofs and Programs (TYPES 2017)},
  pages =	{7:1--7:7},
  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.7},
  URN =		{urn:nbn:de:0030-drops-100553},
  doi =		{10.4230/LIPIcs.TYPES.2017.7},
  annote =	{Keywords: type theory, formalization, category theory, setoids}
}
  • Refine by Author
  • 4 Abel, Andreas
  • 2 Kaposi, Ambrus
  • 2 Nordvall Forsberg, Fredrik
  • 1 Allais, Guillaume
  • 1 Ciccone, Luca
  • Show More...

  • Refine by Classification
  • 6 Theory of computation → Type theory
  • 4 Theory of computation → Proof theory
  • 1 Software and its engineering → Software verification
  • 1 Theory of computation → Categorical semantics
  • 1 Theory of computation → Constructive mathematics
  • Show More...

  • Refine by Keyword
  • 3 type theory
  • 2 Agda
  • 2 Logical Frameworks
  • 2 coinduction
  • 2 natural deduction
  • Show More...

  • Refine by Type
  • 15 document
  • 1 volume

  • Refine by Publication Year
  • 12 2019
  • 2 2021
  • 1 2015
  • 1 2020

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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact