1. http://www.cs.uoregon.edu/Activities/summerschool/summer10/


    - Girard, Lafont and Taylor: Proofs and Types

    - Harper: Practical Foundations for Programming Languages

    - Pierce: Advanced Topics in Types and Programming Languages

    The method of logical relations is a fundamental tool in type theory
    that is used to prove termination and normalization and to analyze
    equations between terms, including parametricity properties for
    polymorphism. The main idea is to interpret types as relations (of a
    suitable class) on terms by associating to each type constructor a
    "relational action" that determines the relation associated to a
    compound type as a function of its constituent types. The
    interpretation is chosen so that well-typed terms stand in the
    relation associated to their type, and so that related terms satisfy a
    property of interest, from which it follows that well-typed terms have
    that property. The method has many applications, but all share the
    characteristic that a global property of terms is reduced to local
    properties of types. I will develop the theory of logical relations
    from first principles, concentrating on two important cases, Goedel's
    System T and Girard's System F.

    # vimeo.com/21048305 Uploaded 496 Plays 0 Comments


Eugene Scherba

Browse This Channel

Shout Box

Heads up: the shoutbox will be retiring soon. It’s tired of working, and can’t wait to relax. You can still send a message to the channel owner, though!

Channels are a simple, beautiful way to showcase and watch videos. Browse more Channels.