A quantitative model for simply typed λ-calculus

Martin Hofmann, Jérémy Ledent

Research output: Contribution to journalArticlepeer-review

16 Downloads (Pure)

Abstract

We use a simplified version of the framework of resource monoids, introduced by Dal Lago and Hofmann (2005, 2011), to interpret simply typed λ -calculus with constants zero and successor. We then use this model to prove a simple quantitative result about bounding the size of the normal form of λ -terms. While the bound itself is already known, this is to our knowledge the first semantic proof of this fact. Our use of resource monoids differs from the other instances found in the literature, in that it measures the size of λ -terms rather than time complexity.
Original languageEnglish
Pages (from-to)777-793
Number of pages18
JournalMathematical Structures in Computer Science
Volume32
Issue numberSpecial Issue 6
Early online date29 Nov 2021
DOIs
Publication statusPublished - 1 Jun 2022

Keywords

  • resource monoid
  • length spaces
  • quantitative semantics
  • lambda calculus

Fingerprint

Dive into the research topics of 'A quantitative model for simply typed λ-calculus'. Together they form a unique fingerprint.

Cite this