Interpreters for Free

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

• Philip Wadler (University of Edinburgh)
• Friday 08 July 2022, 13:30-14:30
• Seminar Room 1, Newton Institute.

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

VS2W01 - Vistas in Verified Software

In a proof assistant based on intuitionistic logic, a standard proof of type soundness automatically yields an interpreter for the corresponding language. This fact is obvious in retrospect, but there is evidence it was not obvious in prospect. The talk describes applications in the textbook Programming Language Foundations in Agda and to the Cardano blockchain. In connection with the latter, we explain why and how Reynolds’s and Girard’s System F, from the 1970s, is used to encode smart contracts that manipulate billions of dollars worth of assets: if you want a system that will still be running in fifty years, use one that is fifty years old!

This talk is part of the Isaac Newton Institute Seminar Series series.

This talk is included in these lists:

• All CMS events
• Featured lists
• INI info aggregator
• Isaac Newton Institute Seminar Series
• School of Physical Sciences
• Seminar Room 1, Newton Institute
• bld31

Note that ex-directory lists are not shown.