[Club2] CLUB2 talk: Dmitriy Traytel -- Wednesday, Oct. 19, 2 PM

[Andrei Popescu]

Dear All, 
On Wednesday, Dmitriy will give us a talk on automatic coercions in Isabelle.  
Dmitriy TraytelExtending Hindley-Milner Type Inference with Coercive Structural Subtyping========================================================Wed. Oct 19, 14:00. Room: von Neumann
Abstract: Coercions allow to convert between different types, and their automatic insertion can greatly increase readability of terms. We presenta type inference algorithm that, given a term without type information,computes a type assignment and determines at which positions in theterm coercions have to be inserted to make it type-correct according tothe standard Hindley-Milner system (without any subtypes). The algo-rithm is sound and, if the subtype relation on base types is a disjointunion of lattices, also complete. The algorithm is used in the proofassistant Isabelle.
Best regards,   Andrei 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20111014/0411676e/attachment.html>