An insider's look at LF type reconstruction: everything you (n)ever wanted to know
Abstract Although type reconstruction for dependently typed languages is common in practical systems, it is still ill-understood. Detailed descriptions of the issues around it are hard to find and formal descriptions together with correctness proofs are non-existing. In this paper, we discuss a one-...
Published in: | Journal of Functional Programming |
---|---|
Main Author: | |
Format: | Article in Journal/Newspaper |
Language: | English |
Published: |
Cambridge University Press (CUP)
2012
|
Subjects: | |
Online Access: | http://dx.doi.org/10.1017/s0956796812000408 https://www.cambridge.org/core/services/aop-cambridge-core/content/view/S0956796812000408 |
id |
crcambridgeupr:10.1017/s0956796812000408 |
---|---|
record_format |
openpolar |
spelling |
crcambridgeupr:10.1017/s0956796812000408 2024-03-03T08:43:11+00:00 An insider's look at LF type reconstruction: everything you (n)ever wanted to know PIENTKA, BRIGITTE 2012 http://dx.doi.org/10.1017/s0956796812000408 https://www.cambridge.org/core/services/aop-cambridge-core/content/view/S0956796812000408 en eng Cambridge University Press (CUP) https://www.cambridge.org/core/terms Journal of Functional Programming volume 23, issue 1, page 1-37 ISSN 0956-7968 1469-7653 Software journal-article 2012 crcambridgeupr https://doi.org/10.1017/s0956796812000408 2024-02-08T08:29:02Z Abstract Although type reconstruction for dependently typed languages is common in practical systems, it is still ill-understood. Detailed descriptions of the issues around it are hard to find and formal descriptions together with correctness proofs are non-existing. In this paper, we discuss a one-pass type reconstruction for objects in the logical framework LF, describe formally the type reconstruction process using the framework of contextual modal types, and prove correctness of type reconstruction. Since type reconstruction will find most general types and may leave free variables, we in addition describe abstraction which will return a closed object where all free variables are bound at the outside. We also implemented our algorithms as part of the Beluga language, and the performance of our type reconstruction algorithm is comparable to type reconstruction in existing systems such as the logical framework Twelf. Article in Journal/Newspaper Beluga Beluga* Cambridge University Press Journal of Functional Programming 23 1 1 37 |
institution |
Open Polar |
collection |
Cambridge University Press |
op_collection_id |
crcambridgeupr |
language |
English |
topic |
Software |
spellingShingle |
Software PIENTKA, BRIGITTE An insider's look at LF type reconstruction: everything you (n)ever wanted to know |
topic_facet |
Software |
description |
Abstract Although type reconstruction for dependently typed languages is common in practical systems, it is still ill-understood. Detailed descriptions of the issues around it are hard to find and formal descriptions together with correctness proofs are non-existing. In this paper, we discuss a one-pass type reconstruction for objects in the logical framework LF, describe formally the type reconstruction process using the framework of contextual modal types, and prove correctness of type reconstruction. Since type reconstruction will find most general types and may leave free variables, we in addition describe abstraction which will return a closed object where all free variables are bound at the outside. We also implemented our algorithms as part of the Beluga language, and the performance of our type reconstruction algorithm is comparable to type reconstruction in existing systems such as the logical framework Twelf. |
format |
Article in Journal/Newspaper |
author |
PIENTKA, BRIGITTE |
author_facet |
PIENTKA, BRIGITTE |
author_sort |
PIENTKA, BRIGITTE |
title |
An insider's look at LF type reconstruction: everything you (n)ever wanted to know |
title_short |
An insider's look at LF type reconstruction: everything you (n)ever wanted to know |
title_full |
An insider's look at LF type reconstruction: everything you (n)ever wanted to know |
title_fullStr |
An insider's look at LF type reconstruction: everything you (n)ever wanted to know |
title_full_unstemmed |
An insider's look at LF type reconstruction: everything you (n)ever wanted to know |
title_sort |
insider's look at lf type reconstruction: everything you (n)ever wanted to know |
publisher |
Cambridge University Press (CUP) |
publishDate |
2012 |
url |
http://dx.doi.org/10.1017/s0956796812000408 https://www.cambridge.org/core/services/aop-cambridge-core/content/view/S0956796812000408 |
genre |
Beluga Beluga* |
genre_facet |
Beluga Beluga* |
op_source |
Journal of Functional Programming volume 23, issue 1, page 1-37 ISSN 0956-7968 1469-7653 |
op_rights |
https://www.cambridge.org/core/terms |
op_doi |
https://doi.org/10.1017/s0956796812000408 |
container_title |
Journal of Functional Programming |
container_volume |
23 |
container_issue |
1 |
container_start_page |
1 |
op_container_end_page |
37 |
_version_ |
1792498603166531584 |