https://hal.inria.fr/inria-00432649Bernardo, BrunoBrunoBernardoLIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau] - X - École polytechnique - CNRS - Centre National de la Recherche ScientifiqueTowards an Implicit Calculus of Inductive Constructions. Extending the Implicit Calculus of Constructions with Union and Subset Types.HAL CCSD2009[INFO.INFO-PL] Computer Science [cs]/Programming Languages [cs.PL]Bernardo, Bruno2009-11-16 18:28:132020-03-05 18:21:582009-11-16 20:46:40enConference papersapplication/pdf1We present extensions of Miquel's Implicit Calculus of Constructions (ICC) and Barras and Bernardo's decidable Implicit Calculus of Constructions (ICC*) with union and subset types. The purpose of these systems is to solve the problem of interaction betweeen logical and computational data. This is a work in progress and our long term goal is to add the whole inductive types to ICC and ICC* in order to define a complete framework for theorem proving.