The Münchhausen Method in Type Theory

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

32 Downloads (Pure)

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.

Original languageEnglish
Title of host publication28th International Conference on Types for Proofs and Programs (TYPES 2022)
EditorsDelia Kesner, Pierre-Marie Pedrot
PublisherSchloss Dagstuhl - Leibniz-Zentrum für Informatik
ISBN (Electronic)9783959772853
DOIs
Publication statusPublished - 28 Jul 2023
Event28th International Conference on Types for Proofs and Programs 2022 - Nantes, France
Duration: 20 Jun 202225 Jun 2022

Publication series

NameLeibniz International Proceedings in Informatics
Volume269
ISSN (Print)1868-8969

Conference

Conference28th International Conference on Types for Proofs and Programs 2022
Abbreviated titleTYPES 2022
Country/TerritoryFrance
CityNantes
Period20/06/2225/06/22

Keywords

  • proof assistants
  • type theory
  • very dependent types

ASJC Scopus subject areas

  • Software

Fingerprint

Dive into the research topics of 'The Münchhausen Method in Type Theory'. Together they form a unique fingerprint.

Cite this