University of Cambridge > > Isaac Newton Institute Seminar Series > Interpreters for Free

Interpreters for Free

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2024, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity