Subject: Coercion Subtyping to the Calculus of Constructions Jour: 12/02/98 (Vendredi 12 juin) http://pauillac.inria.fr/bin/calendar/Seminaires S E M I N A I R E ____ ____ ___ / _ _ / __ __ /_ _ / / | _ __ _ / / \ / \ ___ / / | / /_ / __| / ___ /___/ __| / | __| |___ |_/ |_/ |____ / / __/ |_ |_/ |_ / |_/ / |_/ / / I N R I A - Rocquencourt, Salle de confe'rence du batiment 8 *********** Vendredi 12 juin, 10h30 ---------- Gang Chen ---------- (Ecole Normale Superieur d'Ulm) ==================================================== Coercion Subtyping to the Calculus of Constructions ==================================================== We present a coercion subtyping system to the calculus of constructions (CC). This system is a coercion version of our previous subtyping system to CC. Following the fundamental work of Longo, Milsted and Solovie, we estalish the relationship between coercion subtyping and implication (typing with arrow type). Then, we show how to prove transtivity elimination, coherence, soundness and completeness of coercion. Finally, we present a coercion inference algorithm and its correctness proof.