Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums

Autor: Marcelo Fiore, Vincent Balat, Roberto Di Cosmo
Přispěvatelé: Preuves, Programmes et Systèmes (PPS), Centre National de la Recherche Scientifique (CNRS)-Université Paris Diderot - Paris 7 (UPD7), Computer Laboratory [Cambridge], University of Cambridge [UK] (CAM)
Rok vydání: 2004
Předmět:
Pure mathematics
Normalization property
Computer science
0102 computer and information sciences
02 engineering and technology
Dependent type
01 natural sciences
Lambda cube
Operational semantics
Curry–Howard correspondence
Deductive lambda calculus
Polymorphism (computer science)
Realizability
Calculus of constructions
0202 electrical engineering
electronic engineering
information engineering
computer.programming_language
Simply typed lambda calculus
Type inhabitation
Natural deduction
[INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL]
System F
020207 software engineering
Time-scale calculus
Binary lambda calculus
16. Peace & justice
Fixed-point combinator
Computer Graphics and Computer-Aided Design
Extensional definition
Logical relations
Pure type system
[MATH.MATH-LO]Mathematics [math]/Logic [math.LO]
Type theory
010201 computation theory & mathematics
Church encoding
Lambda calculus
computer
Typed lambda calculus
Algorithm
Software
Normalisation by evaluation
Lambda lifting
Zdroj: Annual Symposium on Principles of Programming Languages
Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages
Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, Jan 2004, pp.64-76, ⟨10.1145/964001.964007⟩
POPL
ISSN: 1558-1160
0362-1340
DOI: 10.1145/982962.964007
Popis: International audience; We present a notion of η-long β-normal term for the typed lambda calculus with sums and prove, using Grothendieck logical relations, that every term is equivalent to one in normal form. Based on this development we give the first type-directed partial evaluator that constructs %able to construct normal forms of terms in this calculus.
Databáze: OpenAIRE
Externí odkaz: