A lambda-calculus with constructors

We present an extension of the λ(η)-calculus with a case construct that propagates through functions like a head linear substitution, and show that this construction permits to recover the expressiveness of ML-style pattern matching. We then prove that this system enjoys the Church-Rosser property u...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Arbiser, A., Miquel, A., Ríos, A.
Formato: SER
Materias:
Artificial intelligence
Computer systems
Pattern matching
Theorem proving
Lambda-calculus
Separation theorems
Difference equations
Acceso en línea:http://hdl.handle.net/20.500.12110/paper_03029743_v4098LNCS_n_p181_Arbiser
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires

Ejemplares similares

Ejemplares similares