BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:The Functional Machine Calculus - Chris Barrett\, University of Bi
 rmingham
DTSTART:20230224T140000Z
DTEND:20230224T150000Z
UID:TALK196921@talks.cam.ac.uk
CONTACT:Jamie Vicary
DESCRIPTION:The Functional Machine Calculus (FMC) was recently introduced 
 by Heijltjes [1] as a generalization of the lambda-calculus to include hig
 her-order global state\, probabilistic and non-deterministic choice\, and 
 input and output\, while retaining confluence. The calculus can encode bot
 h the call-by-name and call-by-value semantics of these effects. This is e
 nabled by two independent generalizations. The first decomposes the syntax
  of the lambda-calculus in a way that allows for the encoding of reduction
  strategies. The second parameterizes application and abstraction in terms
  of `locations’\, which gives a unification of the operational semantics
 \, syntax\, and reduction of the given effects with those of the lambda-ca
 lculus. The FMC further comes equipped with a simple type system which res
 tricts and captures the behaviour of effects\, and guarantees strong norma
 lisation.\n\nThis talk will introduce the FMC and give a summary of its ca
 tegorical semantics [2]. In particular\, an equational theory is introduce
 d\, and shown to be validated by a notion of observational equivalence. Th
 e category of closed FMC-terms modulo this theory\, with composition given
  by sequencing\, then forms the free Cartesian closed category. \n\n[1] Wi
 llem Heijltjes. The Functional Machine Calculus. June 2022. 38th Internati
 onal Conference on Mathematical Foundations of Programming Semantics\, MFP
 S 2022\n\n[2] Chris Barrett\, Willem Heijltjes\, Guy McCusker. The Functio
 nal Machine Calculus II: Semantics. To appear in CSL 2023
LOCATION:SS03\, Computer Laboratory
END:VEVENT
END:VCALENDAR