COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

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-HowardAdd to your list(s) Download to your calendar using vCal - Jamie Gabbay
- Friday 26 September 2008, 14:00-15:00
- Room FW26, Computer Laboratory, William Gates Building.
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 - 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. ## This talk is included in these lists:- All Talks (aka the CURE list)
- Computer Laboratory talks
- Computing and Mathematics
- Interested Talks
- Logic and Semantics Seminar (Computer Laboratory)
- Room FW26, Computer Laboratory, William Gates Building
- School of Technology
- Trust & Technology Initiative - interesting events
- bld31
- yk373's list
Note that ex-directory lists are not shown. |
## Other listssrg The Living Technology Summit - Alibaba, China Railway, ofo, and Alipay Cambridge Statistics Initiative (CSI)## Other talksQuantifying Uncertainty in Turbulent Flow Predictions based on RANS/LES Closures Saving our bumblebees Religion, revelry and resistance in Jacobean Lancashire How to Design a 21st Century Economy - with Kate Raworth Challenges to monetary policy in a global context Designing Active Macroscopic Heat Engines |