Pattern matching and fixed points: Resource types and strong call-by-need

Pablo Barenbaum, Eduardo Bonelli, Kareem Mohamed

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

5 Scopus citations

Abstract

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.

Original languageEnglish
Title of host publicationProceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, PPDP 2018
ISBN (Electronic)9781450364416
DOIs
StatePublished - 3 Sep 2018
Event20th International Symposium on Principles and Practice of Declarative Programming, PPDP 2018 - Frankfurt am Main, Germany
Duration: 3 Sep 20185 Sep 2018

Publication series

NameACM International Conference Proceeding Series

Conference

Conference20th International Symposium on Principles and Practice of Declarative Programming, PPDP 2018
Country/TerritoryGermany
CityFrankfurt am Main
Period3/09/185/09/18

Fingerprint

Dive into the research topics of 'Pattern matching and fixed points: Resource types and strong call-by-need'. Together they form a unique fingerprint.

Cite this