53 Search Results for "Altenkirch, Thorsten"

Volume

LIPIcs, Volume 188

26th International Conference on Types for Proofs and Programs (TYPES 2020)

TYPES 2020, March 2-5, 2020, University of Turin, Italy

Editors: Ugo de'Liguoro, Stefano Berardi, and Thorsten Altenkirch

Volume

LIPIcs, Volume 38

13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)

TLCA 2015, July 1-3, 2015, Warsaw, Poland

Editors: Thorsten Altenkirch

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.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.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.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.MFCS.2021.70
Connecting Constructive Notions of Ordinals in Homotopy Type Theory

Authors: Nicolai Kraus, Fredrik Nordvall Forsberg, and Chuangjie Xu

Published in: LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)

Abstract
In classical set theory, there are many equivalent ways to introduce ordinals. In a constructive setting, however, the different notions split apart, with different advantages and disadvantages for each. We consider three different notions of ordinals in homotopy type theory, and show how they relate to each other: A notation system based on Cantor normal forms, a refined notion of Brouwer trees (inductively generated by zero, successor and countable limits), and wellfounded extensional orders. For Cantor normal forms, most properties are decidable, whereas for wellfounded extensional transitive orders, most are undecidable. Formulations for Brouwer trees are usually partially decidable. We demonstrate that all three notions have properties expected of ordinals: their order relations, although defined differently in each case, are all extensional and wellfounded, and the usual arithmetic operations can be defined in each case. We connect these notions by constructing structure preserving embeddings of Cantor normal forms into Brouwer trees, and of these in turn into wellfounded extensional orders. We have formalised most of our results in cubical Agda.
Cite as

Nicolai Kraus, Fredrik Nordvall Forsberg, and Chuangjie Xu. Connecting Constructive Notions of Ordinals in Homotopy Type Theory. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 70:1-70:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{kraus_et_al:LIPIcs.MFCS.2021.70,
  author =	{Kraus, Nicolai and Nordvall Forsberg, Fredrik and Xu, Chuangjie},
  title =	{{Connecting Constructive Notions of Ordinals in Homotopy Type Theory}},
  booktitle =	{46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},
  pages =	{70:1--70:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-201-3},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{202},
  editor =	{Bonchi, Filippo and Puglisi, Simon J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.70},
  URN =		{urn:nbn:de:0030-drops-145100},
  doi =		{10.4230/LIPIcs.MFCS.2021.70},
  annote =	{Keywords: Constructive ordinals, Cantor normal forms, Brouwer trees}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.TYPES.2020
LIPIcs, Volume 188, TYPES 2020, Complete Volume

Authors: Ugo de'Liguoro, Stefano Berardi, and Thorsten Altenkirch

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

Abstract
LIPIcs, Volume 188, TYPES 2020, Complete Volume
Cite as

Ugo de'Liguoro, Stefano Berardi, and Thorsten Altenkirch. LIPIcs, Volume 188, TYPES 2020, Complete Volume. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 1-204, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@Proceedings{deliguoro_et_al:LIPIcs.TYPES.2020,
  title =	{{LIPIcs, Volume 188, TYPES 2020, Complete Volume}},
  booktitle =	{26th International Conference on Types for Proofs and Programs (TYPES 2020)},
  pages =	{1--204},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020},
  URN =		{urn:nbn:de:0030-drops-138785},
  doi =		{10.4230/LIPIcs.TYPES.2020},
  annote =	{Keywords: LIPIcs, Volume 188, TYPES 2020, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.TYPES.2020.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Ugo de'Liguoro, Stefano Berardi, and Thorsten Altenkirch

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

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

Ugo de'Liguoro, Stefano Berardi, and Thorsten Altenkirch. Front Matter, Table of Contents, Preface, Conference Organization. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 0:i-0:viii, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{deliguoro_et_al:LIPIcs.TYPES.2020.0,
  author =	{de'Liguoro, Ugo and Berardi, Stefano and Altenkirch, Thorsten},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{26th International Conference on Types for Proofs and Programs (TYPES 2020)},
  pages =	{0:i--0:viii},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.0},
  URN =		{urn:nbn:de:0030-drops-138792},
  doi =		{10.4230/LIPIcs.TYPES.2020.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
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.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.TYPES.2020.2
Extending Equational Monadic Reasoning with Monad Transformers

Authors: Reynald Affeldt and David Nowak

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

Abstract
There is a recent interest for the verification of monadic programs using proof assistants. This line of research raises the question of the integration of monad transformers, a standard technique to combine monads. In this paper, we extend Monae, a Coq library for monadic equational reasoning, with monad transformers and we explain the benefits of this extension. Our starting point is the existing theory of modular monad transformers, which provides a uniform treatment of operations. Using this theory, we simplify the formalization of models in Monae and we propose an approach to support monadic equational reasoning in the presence of monad transformers. We also use Monae to revisit the lifting theorems of modular monad transformers by providing equational proofs and explaining how to patch a known bug using a non-standard use of Coq that combines impredicative polymorphism and parametricity.
Cite as

Reynald Affeldt and David Nowak. Extending Equational Monadic Reasoning with Monad Transformers. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 2:1-2:21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{affeldt_et_al:LIPIcs.TYPES.2020.2,
  author =	{Affeldt, Reynald and Nowak, David},
  title =	{{Extending Equational Monadic Reasoning with Monad Transformers}},
  booktitle =	{26th International Conference on Types for Proofs and Programs (TYPES 2020)},
  pages =	{2:1--2: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.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.2},
  URN =		{urn:nbn:de:0030-drops-138810},
  doi =		{10.4230/LIPIcs.TYPES.2020.2},
  annote =	{Keywords: monads, monad transformers, Coq, impredicativity, parametricity}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2020.3
Towards a Certified Reference Monitor of the Android 10 Permission System

Authors: Guido De Luca and Carlos Luna

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

Abstract
Android is a platform for mobile devices that captures more than 85% of the total market share [International Data Corporation (IDC), 2020]. Currently, mobile devices allow people to develop multiple tasks in different areas. Regrettably, the benefits of using mobile devices are counteracted by increasing security risks. The important and critical role of these systems makes them a prime target for formal verification. In our previous work [Betarte et al., 2018], we exhibited a formal specification of an idealized formulation of the permission model of version 6 of Android. In this paper we present an enhanced version of the model in the proof assistant Coq, including the most relevant changes concerning the permission system introduced in versions Nougat, Oreo, Pie and 10. The properties that we had proved earlier for the security model have been either revalidated or refuted, and new ones have been formulated and proved. Additionally, we make observations on the security of the most recent versions of Android. Using the programming language of Coq we have developed a functional implementation of a reference validation mechanism and certified its correctness. The formal development is about 23k LOC of Coq, including proofs.
Cite as

Guido De Luca and Carlos Luna. Towards a Certified Reference Monitor of the Android 10 Permission System. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 3:1-3:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{deluca_et_al:LIPIcs.TYPES.2020.3,
  author =	{De Luca, Guido and Luna, Carlos},
  title =	{{Towards a Certified Reference Monitor of the Android 10 Permission System}},
  booktitle =	{26th International Conference on Types for Proofs and Programs (TYPES 2020)},
  pages =	{3:1--3:18},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.3},
  URN =		{urn:nbn:de:0030-drops-138821},
  doi =		{10.4230/LIPIcs.TYPES.2020.3},
  annote =	{Keywords: Android, Permission model, Formal idealized model, Reference monitor, Formal proofs, Certified implementation, Coq}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2020.4
Coinductive Proof Search for Polarized Logic with Applications to Full Intuitionistic Propositional Logic

Authors: José Espírito Santo, Ralph Matthes, and Luís Pinto

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

Abstract
The approach to proof search dubbed "coinductive proof search", and previously developed by the authors for implicational intuitionistic logic, is in this paper extended to LJP, a focused sequent-calculus presentation of polarized intuitionistic logic, including an array of positive and negative connectives. As before, this includes developing a coinductive description of the search space generated by a sequent, an equivalent inductive syntax describing the same space, and decision procedures for inhabitation problems in the form of predicates defined by recursion on the inductive syntax. We prove the decidability of existence of focused inhabitants, and of finiteness of the number of focused inhabitants for polarized intuitionistic logic, by means of such recursive procedures. Moreover, the polarized logic can be used as a platform from which proof search for other logics is understood. We illustrate the technique with LJT, a focused sequent calculus for full intuitionistic propositional logic (including disjunction). For that, we have to work out the "negative translation" of LJT into LJP (that sees all intuitionistic types as negative types), and verify that the translation gives a faithful representation of proof search in LJT as proof search in the polarized logic. We therefore inherit decidability of both problems studied for LJP and thus get new proofs of these results for LJT.
Cite as

José Espírito Santo, Ralph Matthes, and Luís Pinto. Coinductive Proof Search for Polarized Logic with Applications to Full Intuitionistic Propositional Logic. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 4:1-4:24, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{espiritosanto_et_al:LIPIcs.TYPES.2020.4,
  author =	{Esp{\'\i}rito Santo, Jos\'{e} and Matthes, Ralph and Pinto, Lu{\'\i}s},
  title =	{{Coinductive Proof Search for Polarized Logic with Applications to Full Intuitionistic Propositional Logic}},
  booktitle =	{26th International Conference on Types for Proofs and Programs (TYPES 2020)},
  pages =	{4:1--4:24},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.4},
  URN =		{urn:nbn:de:0030-drops-138837},
  doi =		{10.4230/LIPIcs.TYPES.2020.4},
  annote =	{Keywords: Inhabitation problems, Coinduction, Lambda-calculus, Polarized logic}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2020.5
Synthetic Completeness for a Terminating Seligman-Style Tableau System

Authors: Asta Halkjær From

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

Abstract
Hybrid logic extends modal logic with nominals that name worlds. Seligman-style tableau systems for hybrid logic divide branches into blocks named by nominals to achieve a local proof style. We present a Seligman-style tableau system with a formalization in the proof assistant Isabelle/HOL. Our system refines an existing system to simplify formalization and we claim termination from this relationship. Existing completeness proofs that account for termination are either analytic or based on translation, but synthetic proofs have been shown to generalize to richer logics and languages. Our main result is the first synthetic completeness proof for a terminating hybrid logic tableau system. It is also the first formalized completeness proof for any hybrid logic proof system.
Cite as

Asta Halkjær From. Synthetic Completeness for a Terminating Seligman-Style Tableau System. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 5:1-5:17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{from:LIPIcs.TYPES.2020.5,
  author =	{From, Asta Halkj{\ae}r},
  title =	{{Synthetic Completeness for a Terminating Seligman-Style Tableau System}},
  booktitle =	{26th International Conference on Types for Proofs and Programs (TYPES 2020)},
  pages =	{5:1--5:17},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.5},
  URN =		{urn:nbn:de:0030-drops-138847},
  doi =		{10.4230/LIPIcs.TYPES.2020.5},
  annote =	{Keywords: Hybrid logic, Seligman-style tableau, synthetic completeness, Isabelle/HOL}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2020.6
Encoding of Predicate Subtyping with Proof Irrelevance in the λΠ-Calculus Modulo Theory

Authors: Gabriel Hondet and Frédéric Blanqui

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

Abstract
The λΠ-calculus modulo theory is a logical framework in which various logics and type systems can be encoded, thus helping the cross-verification and interoperability of proof systems based on those logics and type systems. In this paper, we show how to encode predicate subtyping and proof irrelevance, two important features of the PVS proof assistant. We prove that this encoding is correct and that encoded proofs can be mechanically checked by Dedukti, a type checker for the λΠ-calculus modulo theory using rewriting.
Cite as

Gabriel Hondet and Frédéric Blanqui. Encoding of Predicate Subtyping with Proof Irrelevance in the λΠ-Calculus Modulo Theory. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 6:1-6:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{hondet_et_al:LIPIcs.TYPES.2020.6,
  author =	{Hondet, Gabriel and Blanqui, Fr\'{e}d\'{e}ric},
  title =	{{Encoding of Predicate Subtyping with Proof Irrelevance in the \lambda\Pi-Calculus Modulo Theory}},
  booktitle =	{26th International Conference on Types for Proofs and Programs (TYPES 2020)},
  pages =	{6:1--6:18},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.6},
  URN =		{urn:nbn:de:0030-drops-138853},
  doi =		{10.4230/LIPIcs.TYPES.2020.6},
  annote =	{Keywords: Predicate Subtyping, Logical Framework, PVS, Dedukti, Proof Irrelevance}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2020.7
Λ-Symsym: An Interactive Tool for Playing with Involutions and Types

Authors: Furio Honsell, Marina Lenisa, and Ivan Scagnetto

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

Abstract
We present the web portal Λ-symsym, available at http://158.110.146.197:31780/automata/, for experimenting with game semantics of λ^!-calculus, and its normalizing elementary sub-calculus, the λ^{EAL}-calculus. The λ^!-calculus is a generalization of the λ-calculus obtained by introducing a modal operator !, giving rise to a pattern β-reduction. Its sub-calculus corresponds to an applicatively closed class of terms normalizing in an elementary number of steps, in which all elementary functions can be encoded. The game model which we consider is the Geometry of Interaction model I introduced by Abramsky to study reversible computations, consisting of partial involutions over a very simple language of moves. Given a λ^!- or a λ^{EAL}-term, M, Λ-symsym provides: - an abstraction algorithm A^!, for compiling M into a term, A^!(M), of the linear combinatory logic CL^{!}, or the normalizing combinatory logic CL^{EAL}; - an interpretation algorithm [[ ]]^I yielding a specification of the partial involution [[A^!(M)]]^I in the model I; - an algorithm, I2T, for synthesizing from [[A^!(M)]]^I a type, I2T([[A^!(M)]]^I), in a multimodal, intersection type assignment discipline, ⊢_!. - an algorithm, T2I, for synthesizing a specification of a partial involution from a type in ⊢_!, which is an inverse to the former. We conjecture that ⊢_! M : I2T([[A^!(M)]]^I). Λ-symsym permits to investigate experimentally the fine structure of I, and hence the game semantics of the λ^!- and λ^{EAL}-calculi. For instance, we can easily verify that the model I is a λ^!-algebra in the case of strictly linear λ-terms, by checking all the necessary equations, and find counterexamples in the general case. We make this tool available for readers interested to play with games (-semantics). The paper builds on earlier work by the authors, the type system being an improvement.
Cite as

Furio Honsell, Marina Lenisa, and Ivan Scagnetto. Λ-Symsym: An Interactive Tool for Playing with Involutions and Types. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 7:1-7:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{honsell_et_al:LIPIcs.TYPES.2020.7,
  author =	{Honsell, Furio and Lenisa, Marina and Scagnetto, Ivan},
  title =	{{\Lambda-Symsym: An Interactive Tool for Playing with Involutions and Types}},
  booktitle =	{26th International Conference on Types for Proofs and Programs (TYPES 2020)},
  pages =	{7:1--7:18},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.7},
  URN =		{urn:nbn:de:0030-drops-138867},
  doi =		{10.4230/LIPIcs.TYPES.2020.7},
  annote =	{Keywords: game semantics, lambda calculus, involutions, linear logic, implicit computational complexity}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2020.8
Why Not W?

Authors: Jasper Hugunin

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

Abstract
In an extensional setting, 𝚆 types are sufficient to construct a broad class of inductive types, but in intensional type theory the standard construction of even the natural numbers does not satisfy the required induction principle. In this paper, we show how to refine the standard construction of inductive types such that the induction principle is provable and computes as expected in intensional type theory without using function extensionality. We extend this by constructing from 𝚆 an internal universe of codes for inductive types, such that this universe is itself an inductive type described by a code in the next larger universe. We use this universe to mechanize and internalize our refined construction.
Cite as

Jasper Hugunin. Why Not W?. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 8:1-8:9, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{hugunin:LIPIcs.TYPES.2020.8,
  author =	{Hugunin, Jasper},
  title =	{{Why Not W?}},
  booktitle =	{26th International Conference on Types for Proofs and Programs (TYPES 2020)},
  pages =	{8:1--8:9},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.8},
  URN =		{urn:nbn:de:0030-drops-138876},
  doi =		{10.4230/LIPIcs.TYPES.2020.8},
  annote =	{Keywords: dependent types, intensional type theory, inductive types, W types}
}
  • Refine by Author
  • 12 Altenkirch, Thorsten
  • 6 Kaposi, Ambrus
  • 2 Abel, Andreas
  • 2 Berardi, Stefano
  • 2 Capriotti, Paolo
  • Show More...

  • Refine by Classification
  • 12 Theory of computation → Type theory
  • 6 Theory of computation → Proof theory
  • 4 Theory of computation → Logic and verification
  • 3 Security and privacy → Systems security
  • 3 Software and its engineering → Formal software verification
  • Show More...

  • Refine by Keyword
  • 4 Agda
  • 4 dependent types
  • 3 Coq
  • 3 parametricity
  • 3 type theory
  • Show More...

  • Refine by Type
  • 51 document
  • 2 volume

  • Refine by Publication Year
  • 26 2015
  • 15 2021
  • 2 2005
  • 2 2016
  • 2 2019
  • Show More...

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact