Cancelled : Full reduction in the face of absurdity.

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

• Didier Remy - Inria
• Wednesday 20 May 2015, 14:00-15:00
• Lecture Theatre 1, Computer Laboratory.

If you have a question about this talk, please contact David Greaves.

Talk cancelled for today - speaker cannot make it.

Note: Talk cancelled for today – speaker cannot make it. troduces logical assumptions in the type system, which breaks type soundness in the presence of full reduction. Even though programming languages use weak reduction strategies, typically call-by-value, we believe that type soundness for full reduction in the underlying effect-free core calculus is important and gives the programmer a more abstract understanding of program fragments. We propose an expressive type system with implicit coercions and both coherent and incoherent abstraction over coercions. This allows a fine-grained control of dependencies between computations and the logical hypotheses they depend on while preserving the implicit use of hypotheses and confluence. Combining implicit hypotheses and full reduction leads to a better understanding of GAD Ts, provides a better continuum between explicit and implicit type information, and would be a good setting for studying extraction of computational contents from proofs in proof assistants.

Adding GADTs to a language such as ML or System F in

This talk is part of the Wednesday Seminars - Department of Computer Science and Technology series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Chris Davis' list
• Department of Computer Science and Technology talks and seminars
• Graduate-Seminars
• Guy Emerson's list
• Interested Talks
• Lecture Theatre 1, Computer Laboratory
• School of Technology
• Trust & Technology Initiative - interesting events
• Wednesday Seminars - Department of Computer Science and Technology
• bld31
• computer science
• se393's list

Note that ex-directory lists are not shown.