@InProceedings{   10.5555/1754621.1754638,
  Author        = "Filinski, Andrzej",
  Abstract      = "We show how a simple semantic characterization of normalization by evaluation for the {$\lambda$}{$\beta$}η-calculus can be extended to a similar construction for normalization of terms in the computational {$\lambda$}-calculus. Specifically, we show that a suitable residualizing interpretation of base types, constants, and computational effects allows us to extract a syntactic normal form from a term's denotation. The required interpretation can itself be constructed as the meaning of a suitable functional program in an ML-like language, leading directly to a practical normalization algorithm. The results extend easily to product and sum types, and can be seen as a formal basis for call-by-value type-directed partial evaluation.",
  Address       = "Berlin, Heidelberg",
  BookTitle     = "Proceedings of the 5th International Conference on Typed Lambda Calculi and Applications",
  date-added    = "2020-09-25 19:51:07 +0200",
  date-modified = "2020-09-25 19:51:07 +0200",
  ISBN          = "3540419608",
  Location      = "Krak\'{o}w, Poland",
  numpages      = "15",
  Pages         = "151--165",
  Publisher     = "Springer-Verlag",
  Series        = "TLCA'01",
  Title         = "Normalization by Evaluation for the Computational Lambda-Calculus",
  Year          = "2001",
  File          = "Normalization by Evaluation for the Computational Lambda-Calculus - Filinski2001\_Chapter\_NormalizationByEvaluationForTh - a - r.pdf"
}

@InProceedings{ 10.5555/1754621.1754638, Author = "Filinski, Andrzej", Abstract = "We show how a simple semantic characterization of normalization by evaluation for the {$\lambda$}{$\beta$}η-calculus can be extended to a similar construction for normalization of terms in the computational {$\lambda$}-calculus. Specifically, we show that a suitable residualizing interpretation of base types, constants, and computational effects allows us to extract a syntactic normal form from a term's denotation. The required interpretation can itself be constructed as the meaning of a suitable functional program in an ML-like language, leading directly to a practical normalization algorithm. The results extend easily to product and sum types, and can be seen as a formal basis for call-by-value type-directed partial evaluation.", Address = "Berlin, Heidelberg", BookTitle = "Proceedings of the 5th International Conference on Typed Lambda Calculi and Applications", date-added = "2020-09-25 19:51:07 +0200", date-modified = "2020-09-25 19:51:07 +0200", ISBN = "3540419608", Location = "Krak\'{o}w, Poland", numpages = "15", Pages = "151--165", Publisher = "Springer-Verlag", Series = "TLCA'01", Title = "Normalization by Evaluation for the Computational Lambda-Calculus", Year = "2001", File = "Normalization by Evaluation for the Computational Lambda-Calculus - Filinski2001_Chapter_NormalizationByEvaluationForTh - a - r.pdf" }