Change search
ReferencesLink to record
Permanent link

Direct link
Agda Formalisation
Stockholm University, Faculty of Science, Department of Mathematics.
2016 (English)Other (Other academic)Text
Abstract [en]

The following is a formalisation of many of the proofs of arXiv:1610.08027 and arXiv:1612.05468 in Agda. Agda is a proof-checker and programming language based on dependent typetheory and pattern matching, which allow a very close correspondencebetween the style of proofs in the article and the formalised, machine-readable proof.

Place, publisher, year, edition, pages
2016. , 28 p.
Keyword [en]
agda, multisets, homotopy type theory
National Category
Mathematics
Research subject
Mathematical Logic
Identifiers
URN: urn:nbn:se:su:diva-136903OAI: oai:DiVA.org:su-136903DiVA: diva2:1057544
Available from: 2016-12-19 Created: 2016-12-19 Last updated: 2016-12-22Bibliographically approved
In thesis
1. Univalent Types, Sets and Multisets: Investigations in dependent type theory
Open this publication in new window or tab >>Univalent Types, Sets and Multisets: Investigations in dependent type theory
2017 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

This thesis consists of four papers on type theory and a formalisation of certain results from the two first papers in the Agda language. We cover topics such as models of multisets and sets in Homotopy Type Theory, and explore ideas of using type theory as a language for databases and different ways of expressing dependencies between terms. The two first papers build on work by Aczel 1978. We establish that the underlying type of Aczel’s model of set theory in type theory can be seen as a type of multisets from the perspective of Homotopy Type Theory, and we identify a suitable subtype which becomes a model of set theory in which equality of sets is the identity type. The third paper is joint work with Henrik Forssell and David I .Spivak and explores a certain model of type theory, consisting of simplicial complexes, from the perspective of database theory. In the fourth and final paper, we consider two approaches to unraveling the dependency structures between terms in dependent type theory, and formulate a few conjectures about how these two approaches relate.

Place, publisher, year, edition, pages
Stockholm: Department of Mathematics, Stockholm University, 2017. 173 p.
Keyword
type theory, homotopy type theory, dependent types, constructive set theory, databases, formalisation, agda
National Category
Mathematics
Research subject
Mathematics
Identifiers
urn:nbn:se:su:diva-136896 (URN)978-91-7649-654-1 (ISBN)978-91-7649-655-8 (ISBN)
Public defence
2017-02-09, sal 14, hus 5, Kräftriket, Roslagsvägen 101, Stockholm, 13:00 (English)
Opponent
Supervisors
Available from: 2017-01-17 Created: 2016-12-18 Last updated: 2017-01-17Bibliographically approved

Open Access in DiVA

No full text

Other links

Agda files

Search in DiVA

By author/editor
Gylterud, Håkon
By organisation
Department of Mathematics
Mathematics

Search outside of DiVA

GoogleGoogle Scholar

Total: 1 hits
ReferencesLink to record
Permanent link

Direct link