Vers un calcul des constructions pédagogique

Abstract : Pedagogical formal systems have appeared recently for propositional calculus (up to the higher order), and it consists of systematically give examples of introduced notions (hypotheses). Formally, it means that to use a set Delta of formulas as hypotheses, one must first give a substitution sigma such that all the instances of formulas sigma(Delta) can be proved. This neccesity of giving examples has been pointed out by Poincaré (1913) as a common-sense practice: a definition of an object by means of assumptions has interest only if such an object can be constructed. This restriction applied to intuitionistic formal systems is consistent with the idea of negationless mathematics advocated by Griss (1946) in the middle of the past century, and shown as a more radical view of intuitionism. Through the Curry-Howard isomorphism (1980), the computational counterpart is the utility of programs defined in the associated functional systems: every function can be applied to a closed value. First results concerning propositional calculi up to the second-order has recently been published by Colson and Michel (2007, 2008, 2009). In this thesis we present an attempt to standardize and to extend to the Calculus of Constructions (CC) those previous results. First a formal and precise definition of pedagogical sub-systems of the Calculus of Constructions is introduced, and different such sub-systems are exhibited as examples
Document type :
Theses
Complete list of metadatas

Cited literature [49 references]  Display  Hide  Download

https://hal.univ-lorraine.fr/tel-01749591
Contributor : Thèses Ul <>
Submitted on : Thursday, March 29, 2018 - 12:20:38 PM
Last modification on : Wednesday, April 11, 2018 - 1:27:29 AM
Long-term archiving on : Friday, September 14, 2018 - 8:20:45 AM

File

DDOC_T_2012_0388_DEMANGE.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : tel-01749591, version 1

Collections

Citation

Vincent Demange. Vers un calcul des constructions pédagogique. Autre [cs.OH]. Université de Lorraine, 2012. Français. ⟨NNT : 2012LORR0388⟩. ⟨tel-01749591⟩

Share

Metrics

Record views

10

Files downloads

10