|
 
|
[CD11a] Investigations on a Pedagogical Calculus of Constructions
Rapport Scientifique : Date de dépot: 2011/05/16, Nb pages 18, (Tech. Rep.: CEDRIC-11-2736)Mots clés: mathematical logic, negationless mathematics, constructive mathematics, typed lambda-calculus, calculus of constructions, pedagogical system
Résumé:
In the last few years appeared pedagogical propositional natural deduction systems. In these systems, one must satisfy the pedagogical constraint: the user must give an example of any introduced notion. First we expose the reasons of such a constraint and properties of these "pedagogical" calculi: the absence of negation at logical side, and the "usefulness" feature of terms at computational side (through the Curry-Howard correspondence). Then we construct a simple pedagogical restriction of the calculus of constructions (CC) called CCr. We establish logical limitations of this system, and compare its computational expressiveness to Godel system T. Finally, guided by the logical limitations of CCr, we propose a formal and general deï¬nition of what a pedagogical calculus of constructions should be.
Commentaires:
http://hal.archives-ouvertes.fr/hal-00678784
Collaboration:
LITA
BibTeX
| @techreport { | |||
| CD11a, | |||
| title | = | "{Investigations on a Pedagogical Calculus of Constructions}", | |
| author | = | "L. Colson and V. Demange", | |
| number | = | "{CEDRIC-11-2736}", | |
| institution | = | "{CEDRIC laboratory, CNAM-Paris, France}", | |
| date | = | {16-05-2011}, | |
| pages | = | "18", | |
| note | = | "{http://hal.archives-ouvertes.fr/hal-00678784}", | |
| } | |||
