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

Ejemplares similares

Ejemplares similares