Realizability methods allowed to prove normalization results on many typed calculi. Girard adapted these methods to systems of nets and managed to prove normalization of second order Linear Logic [4]. Our contribution is to provide an extension of this proof that embrace Full Differential Linear Logic (a logic that can describe both single-use resources and inexhaustible resources). Anchored within the realizability framework our proof is modular enough so that further extensions (to second order, to additive constructs or to any other independent feature that can be dealt with using realizability) come for free. © 2011 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Gimenez, S. (2011). Realizability proof for normalization of full differential linear logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6690 LNCS, pp. 107–122). https://doi.org/10.1007/978-3-642-21691-6_11
Mendeley helps you to discover research relevant for your work.