On étudie plusieurs voies pour formaliser les quotients dans le Calcul de Constructions Inductive: les quotients naïfs (en utilisant les travaux de {LacasWerner99} et {BarbaneraBerardi96}, on montre qu´ils conduisent à une incohérence), les quotients décidables, les quotients classiques de la théorie des types (comme ceux étudiés dans {Hofmann:thesis}), et finallement on propose une notion de quotients fonctionnels qui résolvent les problèmes des précédentes notions, et semblent satisfaisants théoriquement et pratiquement. Pour chaque notion introduite, on donne la traduction correspondante dans le système \Coq.
Anglais:
To formalize quotients sets in the Calculus of Inductive Constructions, we study several ways: naive quotients (using works of {LacasWerner99} and {BarbaneraBerardi96} we show that they lead to a contradiction), decidable quotients, classical quotients of type theory (as studied in {Hofmann:thesis}), and finally propose a notion of functionnal quotients which solves problems of previous notions of quotient, and seems to be convenient theoretically and practically. For all introduced notions during the paper, we give the corresponding traduction in the system Coq.
Portugais:
Para formalize jogos dos quocientes no cálculo de construções indutivas, nós estudamos diversas maneiras: os quocientes ingénuos (usando trabalhos de { LacasWerner99 } e { BarbaneraBerardi96 } nos mostre que conduzem a um contradiction), os quocientes decidable, quocientes classical da teoria do tipo (como estudado dentro { Hofmann:thesis }), e propõem finalmente uma noção de quocientes do functionnal qual resolva problemas de noções precedentes do quociente, e parecem ser convenientes teòrica e praticamente. Para todas as noções introduzidas durante o papel, nós damos o traduction correspondente no sistema Coq.
Allemand:
um Quotienten Sets im Kalkül der induktiven Aufbauten zu formalisieren, studieren wir einige Weisen: naive Quotienten (mit Arbeiten von { LacasWerner99 } und { BarbaneraBerardi96 } uns zeigen Sie, daß sie zu einen Widerspruch), entscheidbare Quotienten, klassische Quotienten der Arttheorie (wie innen studiert { Hofmann:thesis }) und vorschlagen schließlich einen Begriff der functionnalquotienten welches Probleme vorhergehenden Begriffen des Quotienten löst, und scheinen, bequem zu sein theoretisch und praktisch führen. Für alle eingeführten Begriffe während des Papiers, geben wir den entsprechenden Traduction im System Coq.
Nederlands:
We bestuderen verschillende manieren om quotient verzamelingen formeel te beschrijven in the Calculus van de Inductieve Constructies: naieve quotienten (gebruikmakend van werk van LacasWerner99 en BarbaneraBerardi96 laten we zien dat deze tot een tegenspraak leiden), beslisbare quotienten, klassieke quotienten van type theorie (zoals bestudeerd in het proefschrift van Hofmann), en uiteindelijk komen we met een notie van quotienten die problemen in eerdere noties vermijdt en die zowel theoretisch als practisch goed bruikbaar lijkt. Voor elke geintroduceerde notie geven we de corresponderende beschrijving in het Coq systeem.
Back to schedule.