DROPS

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.TYPES.2022.10

The Münchhausen Method in Type Theory

Authors: Thorsten Altenkirch, Ambrus Kaposi, Artjoms Šinkarovs, and Tamás Végh

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

Abstract

In one of his long tales, after falling into a swamp, Baron Münchhausen salvaged himself and the horse by lifting them both up by his hair. Inspired by this, the paper presents a technique to justify very dependent types. Such types reference the term that they classify, e.g. x : F x. While in most type theories this is not allowed, we propose a technique on salvaging the meaning of both the term and the type. The proposed technique does not refer to preterms or typing relations and works in a completely algebraic setting, e.g categories with families. With a series of examples we demonstrate our technique. We use Agda to demonstrate that our examples are implementable within a proof assistant.

Cite as

Thorsten Altenkirch, Ambrus Kaposi, Artjoms Šinkarovs, and Tamás Végh. The Münchhausen Method in Type Theory. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 10:1-10:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{altenkirch_et_al:LIPIcs.TYPES.2022.10,
  author =	{Altenkirch, Thorsten and Kaposi, Ambrus and \v{S}inkarovs, Artjoms and V\'{e}gh, Tam\'{a}s},
  title =	{{The M\"{u}nchhausen Method in Type Theory}},
  booktitle =	{28th International Conference on Types for Proofs and Programs (TYPES 2022)},
  pages =	{10:1--10:20},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.10},
  URN =		{urn:nbn:de:0030-drops-184534},
  doi =		{10.4230/LIPIcs.TYPES.2022.10},
  annote =	{Keywords: type theory, proof assistants, very dependent types}
}

Document

DOI: 10.4230/LIPIcs.FSCD.2023.18

For the Metatheory of Type Theory, Internal Sconing Is Enough

Authors: Rafaël Bocquet, Ambrus Kaposi, and Christian Sattler

Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)

Abstract

Metatheorems about type theories are often proven by interpreting the syntax into models constructed using categorical gluing. We propose to use only sconing (gluing along a global section functor) instead of general gluing. The sconing is performed internally to a presheaf category, and we recover the original glued model by externalization. Our method relies on constructions involving two notions of models: first-order models (with explicit contexts) and higher-order models (without explicit contexts). Sconing turns a displayed higher-order model into a displayed first-order model. Using these, we derive specialized induction principles for the syntax of type theory. The input of such an induction principle is a boilerplate-free description of its motives and methods, not mentioning contexts. The output is a section with computation rules specified in the same internal language. We illustrate our framework by proofs of canonicity and normalization for type theory.

Cite as

Rafaël Bocquet, Ambrus Kaposi, and Christian Sattler. For the Metatheory of Type Theory, Internal Sconing Is Enough. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 18:1-18:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{bocquet_et_al:LIPIcs.FSCD.2023.18,
  author =	{Bocquet, Rafa\"{e}l and Kaposi, Ambrus and Sattler, Christian},
  title =	{{For the Metatheory of Type Theory, Internal Sconing Is Enough}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{18:1--18:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-277-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{260},
  editor =	{Gaboardi, Marco and van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.18},
  URN =		{urn:nbn:de:0030-drops-180029},
  doi =		{10.4230/LIPIcs.FSCD.2023.18},
  annote =	{Keywords: type theory, presheaves, canonicity, normalization, sconing, gluing}
}

Document

DOI: 10.4230/LIPIcs.FSCD.2023.24

Combinatory Logic and Lambda Calculus Are Equal, Algebraically

Authors: Thorsten Altenkirch, Ambrus Kaposi, Artjoms Šinkarovs, and Tamás Végh

Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)

Abstract

It is well-known that extensional lambda calculus is equivalent to extensional combinatory logic. In this paper we describe a formalisation of this fact in Cubical Agda. The distinguishing features of our formalisation are the following: (i) Both languages are defined as generalised algebraic theories, the syntaxes are intrinsically typed and quotiented by conversion; we never mention preterms or break the quotients in our construction. (ii) Typing is a parameter, thus the un(i)typed and simply typed variants are special cases of the same proof. (iii) We define syntaxes as quotient inductive-inductive types (QIITs) in Cubical Agda; we prove the equivalence and (via univalence) the equality of these QIITs; we do not rely on any axioms, the conversion functions all compute and can be experimented with.

Cite as

Thorsten Altenkirch, Ambrus Kaposi, Artjoms Šinkarovs, and Tamás Végh. Combinatory Logic and Lambda Calculus Are Equal, Algebraically. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 24:1-24:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{altenkirch_et_al:LIPIcs.FSCD.2023.24,
  author =	{Altenkirch, Thorsten and Kaposi, Ambrus and \v{S}inkarovs, Artjoms and V\'{e}gh, Tam\'{a}s},
  title =	{{Combinatory Logic and Lambda Calculus Are Equal, Algebraically}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{24:1--24:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-277-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{260},
  editor =	{Gaboardi, Marco and van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.24},
  URN =		{urn:nbn:de:0030-drops-180086},
  doi =		{10.4230/LIPIcs.FSCD.2023.24},
  annote =	{Keywords: Combinatory logic, lambda calculus, quotient inductive types, Cubical Agda}
}

Document

DOI: 10.4230/LIPIcs.TYPES.2021.6

Internal Strict Propositions Using Point-Free Equations

Authors: István Donkó and Ambrus Kaposi

Published in: LIPIcs, Volume 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021)

Abstract

The setoid model of Martin-Löf’s type theory bootstraps extensional features of type theory from intensional type theory equipped with a universe of definitionally proof irrelevant (strict) propositions. Extensional features include a Prop-valued identity type with a strong transport rule and function extensionality. We show that a setoid model supporting these features can be defined in intensional type theory without any of these features. The key component is a point-free notion of propositions. Our construction suggests that strict algebraic structures can be defined along the same lines in intensional type theory.

Cite as

István Donkó and Ambrus Kaposi. Internal Strict Propositions Using Point-Free Equations. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 6:1-6:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{donko_et_al:LIPIcs.TYPES.2021.6,
  author =	{Donk\'{o}, Istv\'{a}n and Kaposi, Ambrus},
  title =	{{Internal Strict Propositions Using Point-Free Equations}},
  booktitle =	{27th International Conference on Types for Proofs and Programs (TYPES 2021)},
  pages =	{6:1--6:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-254-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{239},
  editor =	{Basold, Henning and Cockx, Jesper and Ghilezan, Silvia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.6},
  URN =		{urn:nbn:de:0030-drops-167759},
  doi =		{10.4230/LIPIcs.TYPES.2021.6},
  annote =	{Keywords: Martin-L\"{o}f’s type theory, intensional type theory, function extensionality, setoid model, homotopy type theory}
}

Document

DOI: 10.4230/LIPIcs.TYPES.2019.6

For Finitary Induction-Induction, Induction Is Enough

Authors: Ambrus Kaposi, András Kovács, and Ambroise Lafont

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

Abstract

Inductive-inductive types (IITs) are a generalisation of inductive types in type theory. They allow the mutual definition of types with multiple sorts where later sorts can be indexed by previous ones. An example is the Chapman-style syntax of type theory with conversion relations for each sort where e.g. the sort of types is indexed by contexts. In this paper we show that if a model of extensional type theory (ETT) supports indexed W-types, then it supports finitely branching IITs. We use a small internal type theory called the theory of signatures to specify IITs. We show that if a model of ETT supports the syntax for the theory of signatures, then it supports all IITs. We construct this syntax from indexed W-types using preterms and typing relations and prove its initiality following Streicher. The construction of the syntax and its initiality proof were formalised in Agda.

Cite as

Ambrus Kaposi, András Kovács, and Ambroise Lafont. For Finitary Induction-Induction, Induction Is Enough. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 6:1-6:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{kaposi_et_al:LIPIcs.TYPES.2019.6,
  author =	{Kaposi, Ambrus and Kov\'{a}cs, Andr\'{a}s and Lafont, Ambroise},
  title =	{{For Finitary Induction-Induction, Induction Is Enough}},
  booktitle =	{25th International Conference on Types for Proofs and Programs (TYPES 2019)},
  pages =	{6:1--6:30},
  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.6},
  URN =		{urn:nbn:de:0030-drops-130707},
  doi =		{10.4230/LIPIcs.TYPES.2019.6},
  annote =	{Keywords: type theory, inductive types, inductive-inductive types}
}

Document

DOI: 10.4230/LIPIcs.FSCD.2020.23

A Syntax for Mutual Inductive Families

Authors: Ambrus Kaposi and Jakob von Raumer

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

Abstract

Inductive families of types are a feature of most languages based on dependent types. They are usually described either by syntactic schemes or by encodings of strictly positive functors such as combinator languages or containers. The former approaches are informal and give only external signatures, the latter approaches suffer from encoding overheads and do not directly represent mutual types. In this paper we propose a direct method for describing signatures for mutual inductive families using a domain-specific type theory. A signature is a context (roughly speaking, a list of types) in this small type theory. Algebras, displayed algebras and sections are defined by models of this type theory: the standard model, the logical predicate and a logical relation interpretation, respectively. We reduce the existence of initial algebras for these signatures to the existence of the syntax of our domain-specific type theory. As this theory is very simple, its normal syntax can be encoded using indexed W-types. To the best of our knowledge, this is the first formalisation of the folklore fact that mutual inductive types can be reduced to indexed W-types. The contents of this paper were formalised in the proof assistant Agda.

Cite as

Ambrus Kaposi and Jakob von Raumer. A Syntax for Mutual Inductive Families. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 23:1-23:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{kaposi_et_al:LIPIcs.FSCD.2020.23,
  author =	{Kaposi, Ambrus and von Raumer, Jakob},
  title =	{{A Syntax for Mutual Inductive Families}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{23:1--23:21},
  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.23},
  URN =		{urn:nbn:de:0030-drops-123451},
  doi =		{10.4230/LIPIcs.FSCD.2020.23},
  annote =	{Keywords: type theory, inductive types, mutual inductive types, W-types, Agda}
}

Document

DOI: 10.4230/LIPIcs.FSCD.2019.25

Gluing for Type Theory

Authors: Ambrus Kaposi, Simon Huber, and Christian Sattler

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

Abstract

The relationship between categorical gluing and proofs using the logical relation technique is folklore. In this paper we work out this relationship for Martin-Löf type theory and show that parametricity and canonicity arise as special cases of gluing. The input of gluing is two models of type theory and a pseudomorphism between them and the output is a displayed model over the first model. A pseudomorphism preserves the categorical structure strictly, the empty context and context extension up to isomorphism, and there are no conditions on preservation of type formers. We look at three examples of pseudomorphisms: the identity on the syntax, the interpretation into the set model and the global section functor. Gluing along these result in syntactic parametricity, semantic parametricity and canonicity, respectively.

Cite as

Ambrus Kaposi, Simon Huber, and Christian Sattler. Gluing for Type Theory. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 25:1-25:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{kaposi_et_al:LIPIcs.FSCD.2019.25,
  author =	{Kaposi, Ambrus and Huber, Simon and Sattler, Christian},
  title =	{{Gluing for Type Theory}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{25:1--25: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.25},
  URN =		{urn:nbn:de:0030-drops-105323},
  doi =		{10.4230/LIPIcs.FSCD.2019.25},
  annote =	{Keywords: Martin-L\"{o}f type theory, logical relations, parametricity, canonicity, quotient inductive 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}
}

20 Search Results for "Kaposi, Ambrus"

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Thanks for your feedback!

Could not send message