Search Results

Documents authored by Altenkirch, Thorsten

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
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

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

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.2019.4
Big Step Normalisation for Type Theory

Authors: Thorsten Altenkirch and Colin Geniet

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

Abstract
Big step normalisation is a normalisation method for typed lambda-calculi which relies on a purely syntactic recursive evaluator. Termination of that evaluator is proven using a predicate called strong computability, similar to the techniques used to prove strong normalisation of β-reduction for typed lambda-calculi. We generalise big step normalisation to a minimalist dependent type theory. Compared to previous presentations of big step normalisation for e.g. the simply-typed lambda-calculus, we use a quotiented syntax of type theory, which crucially reduces the syntactic complexity introduced by dependent types. Most of the proof has been formalised using Agda.
Cite as

Thorsten Altenkirch and Colin Geniet. Big Step Normalisation for Type Theory. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 4:1-4:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{altenkirch_et_al:LIPIcs.TYPES.2019.4,
  author =	{Altenkirch, Thorsten and Geniet, Colin},
  title =	{{Big Step Normalisation for Type Theory}},
  booktitle =	{25th International Conference on Types for Proofs and Programs (TYPES 2019)},
  pages =	{4:1--4:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-158-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{175},
  editor =	{Bezem, Marc and Mahboubi, Assia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.4},
  URN =		{urn:nbn:de:0030-drops-130682},
  doi =		{10.4230/LIPIcs.TYPES.2019.4},
  annote =	{Keywords: Normalisation, big step normalisation, type theory, dependent types, Agda}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2015.3
Towards a Cubical Type Theory without an Interval

Authors: Thorsten Altenkirch and Ambrus Kaposi

Published in: LIPIcs, Volume 69, 21st International Conference on Types for Proofs and Programs (TYPES 2015) (2018)

Abstract
Following the cubical set model of type theory which validates the univalence axiom, cubical type theories have been developed that interpret the identity type using an interval pretype. These theories start from a geometric view of equality. A proof of equality is encoded as a term in a context extended by the interval pretype. Our goal is to develop a cubical theory where the identity type is defined recursively over the type structure, and the geometry arises from these definitions. In this theory, cubes are present explicitly, e.g., a line is a telescope with 3 elements: two endpoints and the connecting equality. This is in line with Bernardy and Moulin's earlier work on internal parametricity. In this paper we present a naive syntax for internal parametricity and by replacing the parametric interpretation of the universe, we extend it to univalence. However, we do not know how to compute in this theory. As a second step, we present a version of the theory for parametricity with named dimensions which has an operational semantics. Extending this syntax to univalence is left as further work.
Cite as

Thorsten Altenkirch and Ambrus Kaposi. Towards a Cubical Type Theory without an Interval. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 3:1-3:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{altenkirch_et_al:LIPIcs.TYPES.2015.3,
  author =	{Altenkirch, Thorsten and Kaposi, Ambrus},
  title =	{{Towards a Cubical Type Theory without an Interval}},
  booktitle =	{21st International Conference on Types for Proofs and Programs (TYPES 2015)},
  pages =	{3:1--3:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-030-9},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{69},
  editor =	{Uustalu, Tarmo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015.3},
  URN =		{urn:nbn:de:0030-drops-84739},
  doi =		{10.4230/LIPIcs.TYPES.2015.3},
  annote =	{Keywords: homotopy type theory, parametricity, univalence}
}
Document
DOI: 10.4230/LIPIcs.CSL.2016.21
Extending Homotopy Type Theory with Strict Equality

Authors: Thorsten Altenkirch, Paolo Capriotti, and Nicolai Kraus

Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

Abstract
In homotopy type theory (HoTT), all constructions are necessarily stable under homotopy equivalence. This has shortcomings: for example, it is believed that it is impossible to define a type of semi-simplicial types. More generally, it is difficult and often impossible to handle towers of coherences. To address this, we propose a 2-level theory which features both strict and weak equality. This can essentially be represented as two type theories: an "outer" one, containing a strict equality type former, and an "inner" one, which is some version of HoTT. Our type theory is inspired by Voevodsky's suggestion of a homotopy type system (HTS) which currently refers to a range of ideas. A core insight of our proposal is that we do not need any form of equality reflection in order to achieve what HTS was suggested for. Instead, having unique identity proofs in the outer type theory is sufficient, and it also has the meta-theoretical advantage of not breaking decidability of type checking. The inner theory can be an easily justifiable extensions of HoTT, allowing the construction of "infinite structures" which are considered impossible in plain HoTT. Alternatively, we can set the inner theory to be exactly the current standard formulation of HoTT, in which case our system can be thought of as a type-theoretic framework for working with "schematic" definitions in HoTT. As demonstrations, we define semi-simplicial types and formalise constructions of Reedy fibrant diagrams.
Cite as

Thorsten Altenkirch, Paolo Capriotti, and Nicolai Kraus. Extending Homotopy Type Theory with Strict Equality. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 21:1-21:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{altenkirch_et_al:LIPIcs.CSL.2016.21,
  author =	{Altenkirch, Thorsten and Capriotti, Paolo and Kraus, Nicolai},
  title =	{{Extending Homotopy Type Theory with Strict Equality}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{21:1--21:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Talbot, Jean-Marc and Regnier, Laurent},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.21},
  URN =		{urn:nbn:de:0030-drops-65612},
  doi =		{10.4230/LIPIcs.CSL.2016.21},
  annote =	{Keywords: homotopy type theory, coherences, strict equality, homotopy type system}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2016.6
Normalisation by Evaluation for Dependent Types

Authors: Thorsten Altenkirch and Ambrus Kaposi

Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)

Abstract
We develop normalisation by evaluation (NBE) for dependent types based on presheaf categories. Our construction is formulated using internal type theory using quotient inductive types. We use a typed presentation hence there are no preterms or realizers in our construction. NBE for simple types is using a logical relation between the syntax and the presheaf interpretation. In our construction, we merge the presheaf interpretation and the logical relation into a proof-relevant logical predicate. We have formalized parts of the construction in Agda.
Cite as

Thorsten Altenkirch and Ambrus Kaposi. Normalisation by Evaluation for Dependent Types. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 6:1-6:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{altenkirch_et_al:LIPIcs.FSCD.2016.6,
  author =	{Altenkirch, Thorsten and Kaposi, Ambrus},
  title =	{{Normalisation by Evaluation for Dependent Types}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{6:1--6:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.6},
  URN =		{urn:nbn:de:0030-drops-59727},
  doi =		{10.4230/LIPIcs.FSCD.2016.6},
  annote =	{Keywords: normalisation by evaluation, dependent types, internal type theory, logical relations, Agda}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.TLCA.2015
LIPIcs, Volume 38, TLCA'15, Complete Volume

Authors: Thorsten Altenkirch

Published in: LIPIcs, Volume 38, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)

Abstract
LIPIcs, Volume 38, TLCA'15, Complete Volume
Cite as

13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@Proceedings{altenkirch:LIPIcs.TLCA.2015,
  title =	{{LIPIcs, Volume 38, TLCA'15, Complete Volume}},
  booktitle =	{13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-87-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{38},
  editor =	{Altenkirch, Thorsten},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015},
  URN =		{urn:nbn:de:0030-drops-52636},
  doi =		{10.4230/LIPIcs.TLCA.2015},
  annote =	{Keywords: Applicative (Functional) Programming, Language Classifications, Language Constructs and Features, Data Structures, Logics and Meanings of Programs Mathematical Logic and Formal Languages, Symbolic and Algebraic Manipulation, Deduction and Theorem Proving}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.TLCA.2015.i
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Thorsten Altenkirch

Published in: LIPIcs, Volume 38, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)

Abstract
This volume contains the papers of the 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015), which was held during 1-3 July 2015, in Warsaw, Poland.
Cite as

13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. i-xii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{altenkirch:LIPIcs.TLCA.2015.i,
  author =	{Altenkirch, Thorsten},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
  pages =	{i--xii},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-87-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{38},
  editor =	{Altenkirch, Thorsten},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.i},
  URN =		{urn:nbn:de:0030-drops-51509},
  doi =		{10.4230/LIPIcs.TLCA.2015.i},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
DOI: 10.4230/LIPIcs.CSL.2012.16
A Syntactical Approach to Weak omega-Groupoids

Authors: Thorsten Altenkirch and Ondrej Rypacek

Published in: LIPIcs, Volume 16, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (2012)

Abstract
When moving to a Type Theory without proof-irrelevance the notion of a setoid has to be generalized to the notion of a weak omega-groupoid. As a first step in this direction we study the formalisation of weak omega-groupoids in Type Theory. This is motivated by Voevodsky's proposal of univalent type theory which is incompatible with proof-irrelevance and the results by Lumsdaine and Garner/van de Berg showing that the standard eliminator for equality gives rise to a weak omega-groupoid.
Cite as

Thorsten Altenkirch and Ondrej Rypacek. A Syntactical Approach to Weak omega-Groupoids. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 16-30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{altenkirch_et_al:LIPIcs.CSL.2012.16,
  author =	{Altenkirch, Thorsten and Rypacek, Ondrej},
  title =	{{A Syntactical Approach to Weak omega-Groupoids}},
  booktitle =	{Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
  pages =	{16--30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-42-2},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{16},
  editor =	{C\'{e}gielski, Patrick and Durand, Arnaud},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.16},
  URN =		{urn:nbn:de:0030-drops-36561},
  doi =		{10.4230/LIPIcs.CSL.2012.16},
  annote =	{Keywords: Type Theory, Category Theory, Higher dimensional structures}
}
Document
DOI: 10.4230/DagSemProc.04381.1
04381 Abstracts Collection – Dependently Typed Programming

Authors: Thorsten Altenkirch, Martin Hofmann, and John Hughes

Published in: Dagstuhl Seminar Proceedings, Volume 4381, Dependently Typed Programming (2005)

Abstract
From 12.09.04 to 17.09.04, the Dagstuhl Seminar 04381 ``Dependently Typed Programming'' was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.
Cite as

Thorsten Altenkirch, Martin Hofmann, and John Hughes. 04381 Abstracts Collection – Dependently Typed Programming. In Dependently Typed Programming. Dagstuhl Seminar Proceedings, Volume 4381, pp. 1-8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2005)

Copy BibTex To Clipboard

@InProceedings{altenkirch_et_al:DagSemProc.04381.1,
  author =	{Altenkirch, Thorsten and Hofmann, Martin and Hughes, John},
  title =	{{04381 Abstracts Collection – Dependently Typed Programming}},
  booktitle =	{Dependently Typed Programming},
  pages =	{1--8},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2005},
  volume =	{4381},
  editor =	{Thorsten Altenkirch and Martin Hofmann and John Hughes},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.04381.1},
  URN =		{urn:nbn:de:0030-drops-1864},
  doi =		{10.4230/DagSemProc.04381.1},
  annote =	{Keywords: dependently typed programming}
}
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