<div class="csl-bib-body">
<div class="csl-entry">Petkovic Komel, A. (2022, July 31). <i>The essence of type-theoretic elaboration</i> [Conference Presentation]. Women In Logic, Haifa, Israel. http://hdl.handle.net/20.500.12708/153703</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/153703
-
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. We define a type-theoretic account of an elaboration map and relate its algorithmic properties to decidability of type-checking.
en
dc.language.iso
en
-
dc.subject
Type theory
en
dc.title
The essence of type-theoretic elaboration
en
dc.type
Presentation
en
dc.type
Vortrag
de
dc.type.category
Conference Presentation
-
tuw.researchTopic.id
C4
-
tuw.researchTopic.id
C5
-
tuw.researchTopic.name
Mathematical and Algorithmic Foundations
-
tuw.researchTopic.name
Computer Science Foundations
-
tuw.researchTopic.value
20
-
tuw.researchTopic.value
80
-
tuw.publication.orgunit
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
tuw.author.orcid
0000-0001-7203-6641
-
tuw.event.name
Women In Logic
en
tuw.event.startdate
31-07-2022
-
tuw.event.enddate
31-07-2022
-
tuw.event.online
On Site
-
tuw.event.type
Event for scientific audience
-
tuw.event.place
Haifa
-
tuw.event.country
IL
-
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.fulltext
no Fulltext
-
item.openairecristype
http://purl.org/coar/resource_type/c_18cp
-
item.languageiso639-1
en
-
item.cerifentitytype
Publications
-
item.openairetype
conference paper not in proceedings
-
item.grantfulltext
none
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
