Linear Abadi and Plotkin Logic
We present a formalization of a version of Abadi and Plotkin's logic for parametricity for a polymorphic dual intuitionistic/linear type theory with fixed points, and show, following Plotkin's suggestions, that it can be used to define a wide collection of types, including existential ty...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2006-11-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/2233/pdf |
| _version_ | 1827322999432282112 |
|---|---|
| author | Lars Birkedal Rasmus E. Møgelberg Rasmus Lerchedahl Petersen |
| author_facet | Lars Birkedal Rasmus E. Møgelberg Rasmus Lerchedahl Petersen |
| author_sort | Lars Birkedal |
| collection | DOAJ |
| description | We present a formalization of a version of Abadi and
Plotkin's logic for parametricity for a polymorphic dual
intuitionistic/linear type theory with fixed points, and show, following
Plotkin's suggestions, that it can be used to define a wide collection of
types, including existential types, inductive types, coinductive types and
general recursive types. We show that the recursive types satisfy a universal
property called dinaturality, and we develop reasoning principles for the
constructed types. In the case of recursive types, the reasoning principle is a
mixed induction/coinduction principle, with the curious property that
coinduction holds for general relations, but induction only for a limited
collection of ``admissible'' relations. A similar property was observed in
Pitts' 1995 analysis of recursive types in domain theory. In a future paper we
will develop a category theoretic notion of models of the logic presented here,
and show how the results developed in the logic can be transferred to the
models. |
| first_indexed | 2024-04-25T01:37:48Z |
| format | Article |
| id | doaj.art-82234fd3648448c19fa1d1a2a9456296 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:37:48Z |
| publishDate | 2006-11-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-82234fd3648448c19fa1d1a2a94562962024-03-08T08:39:02ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742006-11-01Volume 2, Issue 510.2168/LMCS-2(5:2)20062233Linear Abadi and Plotkin LogicLars BirkedalRasmus E. MøgelbergRasmus Lerchedahl PetersenWe present a formalization of a version of Abadi and Plotkin's logic for parametricity for a polymorphic dual intuitionistic/linear type theory with fixed points, and show, following Plotkin's suggestions, that it can be used to define a wide collection of types, including existential types, inductive types, coinductive types and general recursive types. We show that the recursive types satisfy a universal property called dinaturality, and we develop reasoning principles for the constructed types. In the case of recursive types, the reasoning principle is a mixed induction/coinduction principle, with the curious property that coinduction holds for general relations, but induction only for a limited collection of ``admissible'' relations. A similar property was observed in Pitts' 1995 analysis of recursive types in domain theory. In a future paper we will develop a category theoretic notion of models of the logic presented here, and show how the results developed in the logic can be transferred to the models.https://lmcs.episciences.org/2233/pdfcomputer science - logic in computer sciencef.4.1d.3.3 |
| spellingShingle | Lars Birkedal Rasmus E. Møgelberg Rasmus Lerchedahl Petersen Linear Abadi and Plotkin Logic Logical Methods in Computer Science computer science - logic in computer science f.4.1 d.3.3 |
| title | Linear Abadi and Plotkin Logic |
| title_full | Linear Abadi and Plotkin Logic |
| title_fullStr | Linear Abadi and Plotkin Logic |
| title_full_unstemmed | Linear Abadi and Plotkin Logic |
| title_short | Linear Abadi and Plotkin Logic |
| title_sort | linear abadi and plotkin logic |
| topic | computer science - logic in computer science f.4.1 d.3.3 |
| url | https://lmcs.episciences.org/2233/pdf |
| work_keys_str_mv | AT larsbirkedal linearabadiandplotkinlogic AT rasmusemøgelberg linearabadiandplotkinlogic AT rasmuslerchedahlpetersen linearabadiandplotkinlogic |