University of Cambridge > Talks.cam > Logic & Semantics for Dummies > The encode-decode method for equality types

  Browse A-Z

Log in

Googledetails Microsoftdetails

🔐 Log In

Information on

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

ℹī¸ Information

The encode-decode method for equality types

Download to your calendar using vCal

If you have a question about this talk, please contact Alex Rice .

Identity types in Martin-Lof type theory are a powerful tool for reasoning about programs and mathematics. While induction on this type easily allows us to define lots of operations, it can be harder to give a concrete characterisation of the identity type. The encode-decode method is a generic technique for solving this problem.

I will give a recap of the definition of the identity type, describe the encode-decode method and give some examples of it on some basic types before giving a more involved example using univalence.

This talk is part of the Logic & Semantics for Dummies series.

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

Room GS15 at the William Gates Building and on Zoom: https://cl-cam-ac-uk.zoom.us/j/4361570789?pwd=Nkl2T3ZLaTZwRm05bzRTOUUxY3Q4QT09&from=addon Room GS5, Donald McIntyre Building, Faculty of Education, 184 Hills Road, Cambridge, CB2 8PQ B1.19 DAMTP

Other talks

Title to follow Online Causal Inference Seminar LCLU Annual Talk: The Early Aqueous Environment of Mars Inferred From Mission Lifetime Results by the Curiosity Rover at Gale Crater Scattering Plenty: the people who made the modern countryside Title to be confirmed Early cancer clinical trials
 

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