Untyped polarized calculi


We revisit the polarized L calculus, an abstract-machine-like calculus with mixed evaluation order (i.e. call-by-name and call-by-value) and pattern-matches, and its relation to the λ-calculus. We then show that it is a more symmetric syntax for call-by-push-value. We also introduce a dynamically typed / bi-typed variant of this calculus which completely eliminates clashes (i.e. pattern-matching failures) without relying on any form of typing judgments, and illustrate its usefulness in the study of extensions of the untyped λ-calculus with constructors.


  • 22 May 2020: Submission to PPDP 2020
  • 22 June 2020: Rebutal
  • 03 July 2020: Notification, rejected
PhD student