|
| This Article | ||
| ||
| Share | ||
| Bibliographic References | ||
| Add to: | ||
 Digg  Furl  Spurl  Blink  Simpy  Google  Del.icio.us  Y!MyWeb | ||
| Search | ||
| ||
16th Annual IEEE Symposium on Logic in Computer Science (LICS'01)
Normalization by Evaluation for Typed Lambda Calculus with Coproducts
Boston, Massachusetts
June 16-June 19
ISBN: 0-7695-1281-X
| ASCII Text | x | ||
| T. Altenkirch, P. Dybjer, M. Hofmannz, P. Scott, "Normalization by Evaluation for Typed Lambda Calculus with Coproducts," Logic in Computer Science, Symposium on, pp. 0303, 16th Annual IEEE Symposium on Logic in Computer Science (LICS'01), 2001. | |||
| BibTex | x | ||
| @article{ 10.1109/LICS.2001.932506, author = {T. Altenkirch and P. Dybjer and M. Hofmannz and P. Scott}, title = {Normalization by Evaluation for Typed Lambda Calculus with Coproducts}, journal ={Logic in Computer Science, Symposium on}, volume = {0}, year = {2001}, isbn = {0-7695-1281-X}, pages = {0303}, doi = {http://doi.ieeecomputersociety.org/10.1109/LICS.2001.932506}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, } | |||
| RefWorks Procite/RefMan/Endnote | x | ||
| TY - CONF JO - Logic in Computer Science, Symposium on TI - Normalization by Evaluation for Typed Lambda Calculus with Coproducts SN - 0-7695-1281-X SP EP A1 - T. Altenkirch, A1 - P. Dybjer, A1 - M. Hofmannz, A1 - P. Scott, PY - 2001 VL - 0 JA - Logic in Computer Science, Symposium on ER - | |||
Abstract: We solve the decision problem for simply typed lambda calculus with strong binary sums, equivalently the word problem for free cartesian closed categories with binary coproducts. Our method is based on the semantical technique known as "normalization by evaluation" and involves inverting the interpretation of the syntax into a suitable sheaf model and from this extracting appropriate unique normal forms. There is no rewriting theory involved, and the proof is completely constructive, allowing program extraction from the proof.
Citation:
T. Altenkirch, P. Dybjer, M. Hofmannz, P. Scott, "Normalization by Evaluation for Typed Lambda Calculus with Coproducts," lics, pp.0303, 16th Annual IEEE Symposium on Logic in Computer Science (LICS'01), 2001
Usage of this product signifies your acceptance of the Terms of Use.