University of Birmingham > Talks@bham > Lab Lunch > The Scott model of PCF in UniMath

The Scott model of PCF in UniMath

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

If you have a question about this talk, please contact Dr Steve Vickers.

Martin Escardo's talk has been postponed to Friday 22, Sloman Lounge at 11.00

Partiality is not primitive in univalent type theory. One approach to partiality is given by the lifting monad. We will study partiality via lifting by giving a constructive (and predicative) account of the Scott model of PCF in UniMath.

I will briefly introduce PCF , the Scott model as well as soundness and computational adequacy in the traditional setting, for those unfamiliar with this.

Then I will describe the type theoretic details of our constructive account. Propositional truncation will turn out to play a fundamental role. I have proved (and formalised) both soundness and computational adequacy for the constructive model in UniMath.

This talk is part of the Lab Lunch series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on talks.cam from the University of Cambridge.