Semantic evaluation in the simply typed λ-calculus: implicit complexity and normalization

Add to your list(s) Download to your calendar using vCal

• Lê Thành Dũng Nguyễn (Tito)
• Thursday 24 March 2022, 14:00-15:00
• LG23, SoCS and Zoom (see abstract for link).

If you have a question about this talk, please contact Anupam Das.

The idea I want to convey in this presentation is that (effective, finitary) denotational semantics can serve as a tool to compute with λ-terms more efficiently than syntactic rewriting. This will be illustrated through two examples:

• a characterization of regular languages in the simply typed λ-calculus [Hillebrand & Kanellakis, LICS ’96] which is the starting point of the “implicit automata” research programme I will present in the theory seminar next week;
• results on the complexity of normalizing terms of type boolean depending on their type order [Terui, RTA ’12]

==== Zoom details ====

https://bham-ac-uk.zoom.us/j/81873335084?pwd=T1NaUFg2U1l6d0RLL2RlTzFBam1IUT09

Meeting ID: 818 7333 5084 Passcode: 217

This talk is part of the Lab Lunch series.

This talk is included in these lists:

• LG23, SoCS and Zoom (see abstract for link)
• Lab Lunch

Note that ex-directory lists are not shown.