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

  Browse A-Z

Log in

University Account External (via Google)

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹī¸ Information

Interpreters for Free

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.

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

McCrum Lecture Theatre, Bene't Street, next to Eagle pub Winton Programme for the Physics of Sustainability Darwin College (Seminar Room, No. 1 Newnham Terrace - entrance via Porters Lodge on Silver St).

Other talks

The spread of environmental cost-benefit analysis in UK government, c.1966-1995: representing the public in the Anthropocene Title TBC Using Light for Cancer Detection Genomic Medicine CPC Washing machines and their rare components: lessons from kidney patients A Data-Centric Approach to AI Adaptation and Alignment
 

Š 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity