TY - GEN
T1 - Pattern matching and fixed points
T2 - 20th International Symposium on Principles and Practice of Declarative Programming, PPDP 2018
AU - Barenbaum, Pablo
AU - Bonelli, Eduardo
AU - Mohamed, Kareem
N1 - Publisher Copyright:
© 2018 Association for Computing Machinery.
PY - 2018/9/3
Y1 - 2018/9/3
N2 - Resource types are types that statically quantify some aspect of program execution. They come in various guises; this paper focusses on a manifestation of resource types known as non-idempotent intersection types. We use them to characterize weak normalisation for a type-erased lambda calculus for the Calculus of Inductive Construction (λ e ), as introduced by Gregoire and Leroy. The λ e calculus consists of the lambda calculus together with constructors, pattern matching and a fixed-point operator. The characterization is then used to prove the completeness of a strong call-by-need strategy for λ e . This strategy operates on open terms: rather than having evaluation stop when it reaches an abstraction, as in weak call-by-need, it computes strong normal forms by admitting reduction inside the body of abstractions and substitutions. Moreover, argument evaluation is by-need: arguments are evaluated when needed and at most once. Such a notion of reduction is of interest in areas such as partial evaluation and proof-checkers such as Coq.
AB - Resource types are types that statically quantify some aspect of program execution. They come in various guises; this paper focusses on a manifestation of resource types known as non-idempotent intersection types. We use them to characterize weak normalisation for a type-erased lambda calculus for the Calculus of Inductive Construction (λ e ), as introduced by Gregoire and Leroy. The λ e calculus consists of the lambda calculus together with constructors, pattern matching and a fixed-point operator. The characterization is then used to prove the completeness of a strong call-by-need strategy for λ e . This strategy operates on open terms: rather than having evaluation stop when it reaches an abstraction, as in weak call-by-need, it computes strong normal forms by admitting reduction inside the body of abstractions and substitutions. Moreover, argument evaluation is by-need: arguments are evaluated when needed and at most once. Such a notion of reduction is of interest in areas such as partial evaluation and proof-checkers such as Coq.
UR - http://www.scopus.com/inward/record.url?scp=85059850352&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85059850352&partnerID=8YFLogxK
U2 - 10.1145/3236950.3236972
DO - 10.1145/3236950.3236972
M3 - Conference contribution
AN - SCOPUS:85059850352
T3 - ACM International Conference Proceeding Series
BT - Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, PPDP 2018
Y2 - 3 September 2018 through 5 September 2018
ER -