2 Search Results for "Kovacs, Peter"

Document
DOI: 10.4230/LIPIcs.FSCD.2018.20
A Syntax for Higher Inductive-Inductive Types

Authors: Ambrus Kaposi and András Kovács

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

Abstract
Higher inductive-inductive types (HIITs) generalise inductive types of dependent type theories in two directions. On the one hand they allow the simultaneous definition of multiple sorts that can be indexed over each other. On the other hand they support equality constructors, thus generalising higher inductive types of homotopy type theory. Examples that make use of both features are the Cauchy reals and the well-typed syntax of type theory where conversion rules are given as equality constructors. In this paper we propose a general definition of HIITs using a domain-specific type theory. A context in this small type theory encodes a HIIT by listing the type formation rules and constructors. The type of the elimination principle and its beta-rules are computed from the context using a variant of the syntactic logical relation translation. We show that for indexed W-types and various examples of HIITs the computed elimination principles are the expected ones. Showing that the thus specified HIITs exist is left as future work. The type theory specifying HIITs was formalised in Agda together with the syntactic translations. A Haskell implementation converts the types of sorts and constructors into valid Agda code which postulates the elimination principles and computation rules.
Cite as

Ambrus Kaposi and András Kovács. A Syntax for Higher Inductive-Inductive Types. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 20:1-20:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{kaposi_et_al:LIPIcs.FSCD.2018.20,
  author =	{Kaposi, Ambrus and Kov\'{a}cs, Andr\'{a}s},
  title =	{{A Syntax for Higher Inductive-Inductive Types}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{20:1--20:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.20},
  URN =		{urn:nbn:de:0030-drops-91906},
  doi =		{10.4230/LIPIcs.FSCD.2018.20},
  annote =	{Keywords: homotopy type theory, inductive-inductive types, higher inductive types, quotient inductive types, logical relations}
}
Document
DOI: 10.4230/DagSemRep.75
Computational Kinematics (Dagstuhl Seminar 9341)

Authors: Jorge Angeles, Günter Hommer, and Peter Kovacs

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

Jorge Angeles, Günter Hommer, and Peter Kovacs. Computational Kinematics (Dagstuhl Seminar 9341). Dagstuhl Seminar Report 75, pp. 1-24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (1993)

Copy BibTex To Clipboard

@TechReport{angeles_et_al:DagSemRep.75,
  author =	{Angeles, Jorge and Hommer, G\"{u}nter and Kovacs, Peter},
  title =	{{Computational Kinematics (Dagstuhl Seminar 9341)}},
  pages =	{1--24},
  ISSN =	{1619-0203},
  year =	{1993},
  type = 	{Dagstuhl Seminar Report},
  number =	{75},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemRep.75},
  URN =		{urn:nbn:de:0030-drops-149636},
  doi =		{10.4230/DagSemRep.75},
}
  • Refine by Author
  • 1 Angeles, Jorge
  • 1 Hommer, Günter
  • 1 Kaposi, Ambrus
  • 1 Kovacs, Peter
  • 1 Kovács, András

  • Refine by Classification
  • 1 Theory of computation → Type theory

  • Refine by Keyword
  • 1 higher inductive types
  • 1 homotopy type theory
  • 1 inductive-inductive types
  • 1 logical relations
  • 1 quotient inductive types

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 1993
  • 1 2018

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