Factoring Derivation Spaces via Intersection Types

In typical non-idempotent intersection type systems, proof normalization is not confluent. In this paper we introduce a confluent non-idempotent intersection type system for the -calculus. Typing derivations are presented using proof term syntax. The system enjoys good properties: subject reduction,...

Descripción completa

Guardado en:

Detalles Bibliográficos
Autores principales:	Barenbaum, P., Ciruelos, G., Ryu S.
Formato:	SER
Materias:	Derivation space Intersection types Lambda calculus Computation theory Differentiation (calculus) Machinery Garbage-free Semilattices Simulation theorem Strong normalization Subject reduction Calculations
Acceso en línea:	http://hdl.handle.net/20.500.12110/paper_03029743_v11275LNCS_n_p24_Barenbaum
Aporte de:	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires

id	todo:paper_03029743_v11275LNCS_n_p24_Barenbaum
record_format	dspace
spelling	todo:paper_03029743_v11275LNCS_n_p24_Barenbaum2023-10-03T15:18:48Z Factoring Derivation Spaces via Intersection Types Barenbaum, P. Ciruelos, G. Ryu S. Derivation space Intersection types Lambda calculus Computation theory Differentiation (calculus) Machinery Derivation space Garbage-free Intersection types Lambda calculus Semilattices Simulation theorem Strong normalization Subject reduction Calculations In typical non-idempotent intersection type systems, proof normalization is not confluent. In this paper we introduce a confluent non-idempotent intersection type system for the -calculus. Typing derivations are presented using proof term syntax. The system enjoys good properties: subject reduction, strong normalization, and a very regular theory of residuals. A correspondence with the -calculus is established by simulation theorems. The machinery of non-idempotent intersection types allows us to track the usage of resources required to obtain an answer. In particular, it induces a notion of garbage: a computation is garbage if it does not contribute to obtaining an answer. Using these notions, we show that the derivation space of a -term may be factorized using a variant of the Grothendieck construction for semilattices. This means, in particular, that any derivation in the -calculus can be uniquely written as a garbage-free prefix followed by garbage. © 2018, Springer Nature Switzerland AG. SER info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar http://hdl.handle.net/20.500.12110/paper_03029743_v11275LNCS_n_p24_Barenbaum
institution	Universidad de Buenos Aires
institution_str	I-28
repository_str	R-134
collection	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
topic	Derivation space Intersection types Lambda calculus Computation theory Differentiation (calculus) Machinery Derivation space Garbage-free Intersection types Lambda calculus Semilattices Simulation theorem Strong normalization Subject reduction Calculations
spellingShingle	Derivation space Intersection types Lambda calculus Computation theory Differentiation (calculus) Machinery Derivation space Garbage-free Intersection types Lambda calculus Semilattices Simulation theorem Strong normalization Subject reduction Calculations Barenbaum, P. Ciruelos, G. Ryu S. Factoring Derivation Spaces via Intersection Types
topic_facet	Derivation space Intersection types Lambda calculus Computation theory Differentiation (calculus) Machinery Derivation space Garbage-free Intersection types Lambda calculus Semilattices Simulation theorem Strong normalization Subject reduction Calculations
description	In typical non-idempotent intersection type systems, proof normalization is not confluent. In this paper we introduce a confluent non-idempotent intersection type system for the -calculus. Typing derivations are presented using proof term syntax. The system enjoys good properties: subject reduction, strong normalization, and a very regular theory of residuals. A correspondence with the -calculus is established by simulation theorems. The machinery of non-idempotent intersection types allows us to track the usage of resources required to obtain an answer. In particular, it induces a notion of garbage: a computation is garbage if it does not contribute to obtaining an answer. Using these notions, we show that the derivation space of a -term may be factorized using a variant of the Grothendieck construction for semilattices. This means, in particular, that any derivation in the -calculus can be uniquely written as a garbage-free prefix followed by garbage. © 2018, Springer Nature Switzerland AG.
format	SER
author	Barenbaum, P. Ciruelos, G. Ryu S.
author_facet	Barenbaum, P. Ciruelos, G. Ryu S.
author_sort	Barenbaum, P.
title	Factoring Derivation Spaces via Intersection Types
title_short	Factoring Derivation Spaces via Intersection Types
title_full	Factoring Derivation Spaces via Intersection Types
title_fullStr	Factoring Derivation Spaces via Intersection Types
title_full_unstemmed	Factoring Derivation Spaces via Intersection Types
title_sort	factoring derivation spaces via intersection types
url	http://hdl.handle.net/20.500.12110/paper_03029743_v11275LNCS_n_p24_Barenbaum
work_keys_str_mv	AT barenbaump factoringderivationspacesviaintersectiontypes AT ciruelosg factoringderivationspacesviaintersectiontypes AT ryus factoringderivationspacesviaintersectiontypes
_version_	1807323295970754560

Factoring Derivation Spaces via Intersection Types

Ejemplares similares