<div class="csl-bib-body">
<div class="csl-entry">Petkovic Komel, A. (2022, May 20). <i>The essence of elaboration</i> [Conference Presentation]. Workshop on Syntax and Semantics of Type Thoery, Stockholm, Sweden. http://hdl.handle.net/20.500.12708/153774</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/153774
-
dc.description.abstract
When using type theories in proof assistants the full syntax can quickly become too verbose to handle. One common solution to this problem is to design two type theories: a fully annotated type theory which has good meta-theoretic properties, is suitable for algorithmic processing and resides in the kernel of the proof assistant, and an economic one for the users’ input. The two theories are linked by elaboration, a reconstruction of missing information that happens during, or in parallel with, type-checking.
In this talk we will take a look at the type-theoretic account of an elaboration map: a section of a “forgetful” type-theoretic transformation $r : S \to T$ from the fully annotated type theory S, which we will call standard type theory, to the economic one T, called a finitary type theory. This definition of elaboration map enjoys two important meta-theoretic properties: every finitary type theory has an elaboration map to a standard type theory and it satisfies a universal property, making it unique up-to judgemental equality. We will also consider algorithmic aspects of elaboration and relate it to type-checking.
This is joint work with Andrej Bauer.
en
dc.description.sponsorship
European Commission
-
dc.language.iso
en
-
dc.subject
Type Theory
en
dc.subject
Elaboration
en
dc.subject
Type Checking
en
dc.title
The essence of elaboration
en
dc.type
Presentation
en
dc.type
Vortrag
de
dc.relation.grantno
ERC Consolidator Grant 2020
-
dc.type.category
Conference Presentation
-
tuw.publication.invited
invited
-
tuw.project.title
Automated Reasoning with Theories and Induction for Software Technologies
-
tuw.researchTopic.id
C4
-
tuw.researchTopic.id
C5
-
tuw.researchTopic.name
Mathematical and Algorithmic Foundations
-
tuw.researchTopic.name
Computer Science Foundations
-
tuw.researchTopic.value
40
-
tuw.researchTopic.value
60
-
tuw.publication.orgunit
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
tuw.author.orcid
0000-0001-7203-6641
-
tuw.event.name
Workshop on Syntax and Semantics of Type Thoery
en
tuw.event.startdate
20-05-2022
-
tuw.event.enddate
21-05-2022
-
tuw.event.online
On Site
-
tuw.event.type
Event for scientific audience
-
tuw.event.place
Stockholm
-
tuw.event.country
SE
-
tuw.event.presenter
Petkovic Komel, Anja
-
wb.sciencebranch
Informatik
-
wb.sciencebranch
Mathematik
-
wb.sciencebranch.oefos
1020
-
wb.sciencebranch.oefos
1010
-
wb.sciencebranch.value
60
-
wb.sciencebranch.value
40
-
item.languageiso639-1
en
-
item.openairetype
conference paper not in proceedings
-
item.grantfulltext
none
-
item.fulltext
no Fulltext
-
item.cerifentitytype
Publications
-
item.openairecristype
http://purl.org/coar/resource_type/c_18cp
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
