This talk raises the question of whether we should go back to denotational semantics. I suspect that the elementary models of the λ-calculus (graph models and filter models) did not get a fair shake. These semantics are much simpler than the standard models and can be just as simple to define as an operational semantics. But why should we give up operational semantics? Denotational semantics have two properties that are lacking in operational semantics: they are compositional and extensional. In this talk I’ll present a new variation on the elementary models of the λ-calculus and discuss applications to compiler correctness and handling features such as parametric polymorphism. Of course, this just scratches the surface regarding whether this style of semantics is easier to use for large-scale language mechanization efforts. I invite you to join me as I go back to the future with denotational semantics!

Jeremy Siek is an Associate Professor at Indiana University Bloomington. Jeremy’s areas of research include programming language design, type systems, mechanized theorem proving using proof assistants, and optimizing compilers. Jeremy’s Ph.D. thesis explored foundations for constrained templates, aka the “concepts” proposal for C++. Prior to that, Jeremy developed the Boost Graph Library, a C++ generic library for graph algorithms and data structures. Jeremy post-doc’d at Rice University where he developed the idea of gradual typing: a type system that integrates both dynamic and static typing in the same programming language. Jeremy is currently working on several open questions regarding gradual typing. Is the polymorphic blame calculus really parametric? How should gradual typing be combined with other features such as dependent types? What is the formal criteria for gradually typed languages? Is it possible to create a high-performance implementation of a gradually-typed languages? In 2009 Jeremy received the NSF CAREER award to fund his project: “Bridging the Gap Between Prototyping and Production”. In 2010 and again in 2015, Jeremy was awarded a Distinguished Visiting Fellowship from the Scottish Informatics & Computer Science Alliance.