University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > Nominal terms and one-and-a-half level Curry-Howard

Nominal terms and one-and-a-half level Curry-Howard

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

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

The Curry-Howard correspondence equates propositions with types and derivations with lambda-terms. The lambda-calculus does not immediately provide terms to correspond to incomplete derivations—- derivations containing “holes”. Solutions include lambda-lifting; I will show how a suitable notion of typed nominal term can also represent incomplete terms and give a nice Curry-Howard correspondence which very precisely matches what we do when we fill in a proof on a piece of paper. The typing system is quite sophisticated, corresponding with first-order logic.

An overview is as follows:
  • Types correspond with first-order logic predicates.
  • Terms correspond with incomplete proofs.
  • Level 1 variables (atoms) correspond with assumptions; types of the variables correspond with predicates assumed.
  • Level 2 variables (unknowns) correspond with unknown parts of the derivation.
  • A notion of beta-reduction for level 1 variables corresponds with proof-normalisation.
  • Instantiation of level 2 variables corresponds with filling in more of the derivation.

Full details are in my conference paper with Mulligan and more information, including slides of the talk (before the talk, if I’m really efficient) can be found on my homepage.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

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