Relating System F and Lambda2: A Case Study in Coq, Abella and Beluga
We give three formalisations of a proof of the equivalence of the usual, two-sorted presentation of System F and its single-sorted pure type system (PTS) variant Lambda2. This is established by reducing the typability problem of F to Lambda2 and vice versa. A key challenge is the treatment of variab...
Main Authors: | , , |
---|---|
Format: | Conference Object |
Language: | English |
Published: |
Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik
2017
|
Subjects: | |
Online Access: | https://doi.org/10.4230/LIPIcs.FSCD.2017.21 https://nbn-resolving.org/urn:nbn:de:0030-drops-77248 https://drops.dagstuhl.de/opus/volltexte/2017/7724/ |
id |
ftdagstuhl:oai:drops-oai.dagstuhl.de:7724 |
---|---|
record_format |
openpolar |
spelling |
ftdagstuhl:oai:drops-oai.dagstuhl.de:7724 2023-05-15T15:41:45+02:00 Relating System F and Lambda2: A Case Study in Coq, Abella and Beluga Kaiser, Jonas Pientka, Brigitte Smolka, Gert 2017 application/pdf https://doi.org/10.4230/LIPIcs.FSCD.2017.21 https://nbn-resolving.org/urn:nbn:de:0030-drops-77248 https://drops.dagstuhl.de/opus/volltexte/2017/7724/ eng eng Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik LIPIcs - Leibniz International Proceedings in Informatics. 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017) doi:10.4230/LIPIcs.FSCD.2017.21 urn:nbn:de:0030-drops-77248 https://drops.dagstuhl.de/opus/volltexte/2017/7724/ https://creativecommons.org/licenses/by/3.0/ CC-BY Pure Type Systems System F de Bruijn Syntax Higher-Order Abstract Syntax Contextual Reasoning Data processing Computer science InProceedings publishedVersion 2017 ftdagstuhl https://doi.org/10.4230/LIPIcs.FSCD.2017.21 2022-05-23T15:17:18Z We give three formalisations of a proof of the equivalence of the usual, two-sorted presentation of System F and its single-sorted pure type system (PTS) variant Lambda2. This is established by reducing the typability problem of F to Lambda2 and vice versa. A key challenge is the treatment of variable binding and contextual information. The formalisations all share the same high level proof structure using relations to connect the type systems. They do, however, differ significantly in their representation and manipulation of variables and contextual information. In Coq, we use pure de Bruijn indices and parallel substitutions. In Abella, we use higher-order abstract syntax (HOAS) and nominal constants of the ambient reasoning logic. In Beluga, we also use HOAS but within contextual modal type theory. Our contribution is twofold. First, we present and compare a collection of machine-checked solutions to a non-trivial theoretical result. Second, we propose our proof as a benchmark, complementing the POPLmark and ORBI challenges by testing how well a given proof assistant or framework handles complex contextual information involving multiple type systems. Conference Object Beluga Beluga* DROPS - Dagstuhl Research Online Publication Server (Schloss Dagstuhl - Leibniz Center for Informatics ) |
institution |
Open Polar |
collection |
DROPS - Dagstuhl Research Online Publication Server (Schloss Dagstuhl - Leibniz Center for Informatics ) |
op_collection_id |
ftdagstuhl |
language |
English |
topic |
Pure Type Systems System F de Bruijn Syntax Higher-Order Abstract Syntax Contextual Reasoning Data processing Computer science |
spellingShingle |
Pure Type Systems System F de Bruijn Syntax Higher-Order Abstract Syntax Contextual Reasoning Data processing Computer science Kaiser, Jonas Pientka, Brigitte Smolka, Gert Relating System F and Lambda2: A Case Study in Coq, Abella and Beluga |
topic_facet |
Pure Type Systems System F de Bruijn Syntax Higher-Order Abstract Syntax Contextual Reasoning Data processing Computer science |
description |
We give three formalisations of a proof of the equivalence of the usual, two-sorted presentation of System F and its single-sorted pure type system (PTS) variant Lambda2. This is established by reducing the typability problem of F to Lambda2 and vice versa. A key challenge is the treatment of variable binding and contextual information. The formalisations all share the same high level proof structure using relations to connect the type systems. They do, however, differ significantly in their representation and manipulation of variables and contextual information. In Coq, we use pure de Bruijn indices and parallel substitutions. In Abella, we use higher-order abstract syntax (HOAS) and nominal constants of the ambient reasoning logic. In Beluga, we also use HOAS but within contextual modal type theory. Our contribution is twofold. First, we present and compare a collection of machine-checked solutions to a non-trivial theoretical result. Second, we propose our proof as a benchmark, complementing the POPLmark and ORBI challenges by testing how well a given proof assistant or framework handles complex contextual information involving multiple type systems. |
format |
Conference Object |
author |
Kaiser, Jonas Pientka, Brigitte Smolka, Gert |
author_facet |
Kaiser, Jonas Pientka, Brigitte Smolka, Gert |
author_sort |
Kaiser, Jonas |
title |
Relating System F and Lambda2: A Case Study in Coq, Abella and Beluga |
title_short |
Relating System F and Lambda2: A Case Study in Coq, Abella and Beluga |
title_full |
Relating System F and Lambda2: A Case Study in Coq, Abella and Beluga |
title_fullStr |
Relating System F and Lambda2: A Case Study in Coq, Abella and Beluga |
title_full_unstemmed |
Relating System F and Lambda2: A Case Study in Coq, Abella and Beluga |
title_sort |
relating system f and lambda2: a case study in coq, abella and beluga |
publisher |
Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik |
publishDate |
2017 |
url |
https://doi.org/10.4230/LIPIcs.FSCD.2017.21 https://nbn-resolving.org/urn:nbn:de:0030-drops-77248 https://drops.dagstuhl.de/opus/volltexte/2017/7724/ |
genre |
Beluga Beluga* |
genre_facet |
Beluga Beluga* |
op_relation |
doi:10.4230/LIPIcs.FSCD.2017.21 urn:nbn:de:0030-drops-77248 https://drops.dagstuhl.de/opus/volltexte/2017/7724/ |
op_rights |
https://creativecommons.org/licenses/by/3.0/ |
op_rightsnorm |
CC-BY |
op_doi |
https://doi.org/10.4230/LIPIcs.FSCD.2017.21 |
_version_ |
1766374647902765056 |