[msp-interest] [MSP101] Kostia Chardonnet: Approximation Theory for Distant Bang Calculus (1pm Tue 15/9, LT210)

[Emma Tye]

Dear all,

We have another MSP101 seminar coming up. Hope to see you there!

Best wishes,
Emma

Date, time and place:
  Tuesday 15 September, 13:00, Livingstone Tower room LT210

Online attendance:
  https://www.youtube.com/channel/UC3IBMh699qT5wawP3nHRItg/live

Speaker:
  Kostia Chardonnet (INRIA Nancy)

Title:
  Approximation Theory for Distant Bang Calculus

Abstract:
  Approximation semantics capture the observable behaviour of λ-terms. Böhm Trees and Taylor Expansion are their two central paradigms, related by the Commutation Theorem. While these notions are well understood in Call-by-Name (CbN), they have only recently been developed for Call-by-Value (CbV). However, these notions require a separate development for each evaluation strategy of the λ-calculus, which motivates the search for a unified approximation framework. The Bang-calculus provides such a framework: it subsumes both CbN and CbV through linear-logic translations and enjoys robust rewriting properties. We develop the approximation semantics of dBang (the Bang-calculus with explicit substitutions and distant reductions) by introducing approximation trees in the Böhm tradition together with Taylor expansion. We establish their fundamental properties, including a commutation theorem. Via translations, our results recover the CbN and CbV setting within a single unifying framework capturing infinitary and resource-sensitive semantics.

MSP101 Feeds:
  Web: http://msp.cis.strath.ac.uk/msp101.html
  RSS: http://msp.cis.strath.ac.uk/msp101.rss
 iCal: http://msp.cis.strath.ac.uk/msp101.ics