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: | Lars Birkedal, Rasmus E. Møgelberg, Rasmus Lerchedahl Petersen |
---|---|
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 |
Similar Items
-
Linear-use CPS translations in the Enriched Effect Calculus
by: Jeff Egger, et al.
Published: (2012-10-01) -
Logical Step-Indexed Logical Relations
by: Derek Dreyer, et al.
Published: (2011-06-01) -
Game semantics for first-order logic
by: Olivier Laurent
Published: (2010-10-01) -
A Logical Foundation for Environment Classifiers
by: Takeshi Tsukada, et al.
Published: (2010-12-01) -
Relational Parametricity for Computational Effects
by: Rasmus Ejlers Møgelberg, et al.
Published: (2009-08-01)