bienvenue sur ma page personnelle
bienvenue sur ma page personnelle
rené david
professeur
(dernière mise à jour : 17/09/2007)
in my
office
outside my office
informations diverses
equipe de recherche : logique
numéro de bureau : 105
tel : 33 (0)4 79 75 87 17 fax : 33 (0)4
79 75 81 42
email : rene.david@univ-savoie.fr
thèmes de recherche
lambda calcul pur et typé
théorie de la démonstration
conférences
conférence donnée les
20 avril 2004 à
chambéry et 22 avril 2004 à annecy dans le cadre "amphis
pour tous"
"peut-on
faire des mathématiques avec un ordinateur" le fichier associé à ce lien est un fichier.htm. je
peux
aussi, à la demande, vous fournir le fichier.ppt
conférence donnée les 16 mai 2007 à
thonon, 22 mai 2007 à chambéry et 24 mai 2007 à annecy dans le cadre "amphis
pour tous"
"peut-on avoir confiance en l'informatique ?" le fichier associé est un fichier pdf.
liens
i am the co-organizer (with laurence vignollet)
of the 2nd
international
doctoral school
"chambéry - torino"
in theoretical computer science and in semantic web
21-25, june 2004 aussois (savoie - france) aussois
school
pour récupérer phox, l'assistant de preuves de c. raffalli que
nous utilisons avec les étudiants dans un but
pédagogique, cliquez ici
planning
des
séminaires de l'équipe de logique.
co-organisateur du workshop
chambéry-cracovie-lyon "computational logic and applications".
le bourget du lac, 20-21 juin 2005.
i am the co-organizer (with laurence vignollet, simona ronchi della rocca and cristina baroglio)
of the third international doctoral school chambéry - torino
in theoretical computer science and/or service-oriented
architectures from august 28th to september 1st in torino. i gave
a course. my slides are here
i am the organizer of the next meeting of the group lac (logique,
algèbre et calcul) of the gdr im (informatique
mathématique) at chambéry on 8-9 february 2007. more information here
publications (enseignement)
r. david, k. nour et c. raffalli introduction à la logique.
théorie de la
démonstration. cours et exercices corrigés.
cet ouvrage, entièrement
révisé dans cette seconde
édition, est un
cours introductif à la logique mathématique et, en
particulier, la
théorie de la démonstration. on y donne la réponse
du mathématicien aux
questions " qu'est-ce qu'un énoncé ? une
démonstration ? " ou plus
fondamentalement, " qu'est-ce que les mathématiques ? ", en
l'illustrant par de nombreux exemples de mathématiques
courantes. il
aborde également la logique intuitionniste qui donne des preuves
constructives et les techniques de base de la démonstration
automatique. ces notions sont essentielles en informatique.
pour
aider le lecteur dans sa compréhension, ce cours contient de
nombreux
exemples et près de 170 exercices corrigés. une annexe
présente un
assistant de démonstration, le logiciel phox, écrit par
l'un des
auteurs. des compléments aux corrigés (preuves
complètement formalisées
ou réalisées avec le logiciel phox) ainsi que le logiciel
phox, sont
disponibles sur le site des auteurs.
ce livre, qui ne suppose
aucun prérequis en logique, s'adresse plus
particulièrement aux
étudiants en 3e année de licence ou en master. il pourra
également
intéresser les candidats au capes et à
l'agrégation.
r.david & c raffalli : apprentissage du
raisonnement assisté par ordinateur.
une
version courte short.ps
est parue dans la
gazette des mathématiciens (n° 92 avril 2002) et une version
longue long.ps
incluant une présentation générale de phox
est parue dans la revue quadrature (n° 45 printemps 2002).
we
describe our experience of using phox (the prover of c
raffalli) with undergraduate students in mathematics.
r.david : une
expérience de preuves sur ordinateur avec des étudiants
de licence. revue de maths
spé n° 4 (2002- 2003) p 454-471. rmc
during the 2002-03 academic year, i used phox (the prover of c
raffalli) with the undergraduate students in mathematics (in
third year) to help them to do correct proofs. they proved,
among
other things, heine's theorem. in this paper i describe this very
promising experience.
r.david & c
raffalli : an experiment concerning mathematical proofs on computers
with french undergraduate students. (journal of applied
logic, vol 2 n°2 p 219-239, 2004 ) experiment.ps
a synthesis of the two previous papers.
r.david & c
raffalli : some considerations about proof assistants for education. pate07.pdf
a talk given at the pate workshop during rdp'07
publications (recherche)
r. david & k. nour : an arithmetical proof of the strong normalization
results for the lambda -calculus with recursive equations on types. lncs 4583 p 84-101 tlca'07 tlca'07.
we give an arithmetical proof of the strong normalization of the
lambda-calculus (and also of the lambda-mu-calculus) where the type
system is the one of simple types with recursive equations on
types.
the proof using candidates of reducibility is an easy extension
of the one without equations but this proof cannot be formalized
in peano arithmetic. the strength of the system needed for such a
proof was not known. our proof shows that it is not more than
peano arithmetic.
r. david & k. nour : arithmetical proofs of strong normalization
results for the symmetric lambda mu-calculus. tlca'05. lncs 3461 p 162-178 tlca'05.
the symmetric lambda
mu-calculus is the lambda mu-calculus introduced by parigot in which
the reduction rule mu', which is the symmetric of mu, is added. we give
arithmetical proofs of some strong normalization results for this
calculus. we show that the mu mu'-reduction is strongly normalizing for
the un-typed calculus. we also show the strong normalization of the
beta mu mu'-reduction for the typed calculus: this was already known
but the previous proofs use candidates of reducibility where the
interpretation of a type was defined as the fix point of someincreasing
operator and thus, were highly non arithmetical.
r.david & k. nour : why the usual candidates of reducibility do
not work for the symmetric lambda mu calculus. entcs
140 p 101-11 (2005). cla'05
the symmetric lambda
mu-calculus is the lambda mu-calculus
introduced by parigot in which the reduction rule mu', which is the
symmetric of mu, is added. we give examples explaining why the
technique using the usual candidates of reducibility does not work. we
also prove a standardization theorem for this calculus.
r. david & k. nour : a short proof of the
strong normalization of the simply typed lambda mu calculus. schedae
informaticae n°12 (2003) p 27-34 lambda
mu.ps
we give a very short proof of the strong normalization of the
simply
typed lambda mu calculus.
r. david & g. mounier : an intuitionistic
lambda calculus with exceptions. journal of functional
programming. 15 (1) p 33-52 (2005) ex2.ps
we introduce a
lambda calculus which allows the use of exceptions in the ml style.
r. david & k. nour
: a short proof of the strong normalization of classical natural
deduction with disjunction. jsl vol 68 n° 4 p 1277-1288 (2003)
. sn_dednat.ps
we give a
arithmetical proof of the strong normalization of the cut elimination
procedure in full and classical natural
deduction i.e. with the absurdity rule and all the usual connectives
with their intuitionistic meaning.
r. david : decidabilty results for primitive
recursive algorithms. tcs n°300/1-3 (2003) p 477-504. deci.ps
i give some results, extending
the old ones of t. coquand and l. colson, about the decidabilty of
problems related to primitive recursive algorithms.
r. david & b. guillaume : stong
normalization of the typed lambda_ws calculus : csl'03 (lncs 2803 p
155-168) csl.ps
we give a characterization of
strongly normalizable terms. we deduce an arithmetical proof of the
simply typed calculus and a proof (using reducibility candidates) of
the second order typed calculus.
r. david : computing with böhm
trees comp.ps
: fundamenta informaticae 45 (1,2) p 53-77 (2001).
i develop a technic to
compute with böhm trees. this gives a proof of r.kerth's
conjecture on unsolvable terms. this also gives a syntactical proof of
hyland and wadsworth's theorem.
r. david : on the asymptotic behaviour
of primitive recursive algorithms
asym.ps.gz : tcs n° 266 (2001) p 159-193.
i define the notion of trace for
primitive recursive algorithms. this gives a new proof of colson's
theorem and extend it to the case where mutual recursion is allowed.
i use this notion to prove a property (called the backtracking
property) satisfied by any primitive recursive algorithm using any
kind of data type (colson's theorem is valid only with the integers in
unary notation).
r. david & b. guillaume : a lambda-calculus with
explicit weakening and
explicit substitution mscs.ps
: mscs vol 11 (2001) p 169-206.
a calculus with explicit
substitutions satisfying the following properties : confluence on open
terms, step by step simulation of beta,
preservation of the strong normalization, strong normalization of
the calculus of substitution.
r. david : normalization without
reducibility. apal n° 107 (2001) p 121-130. normal.ps
an elementary (and purely
arithmetical) proof of results relating typability in the intersection
type discipline and various notions of normalization. this
contains, in particular, the next paper wich is extracted from this one.
r. david : a short proof of the strong
normalization of the simply typed lambda calculus. sn.ps
i give a half page proof a the
strong normalization of the simply typed lambda calculus
r.david & w.py : lambda-mu-calculus and böhm's
theorem bohm.ps
: jsl 66. 1 (2001) p 407-413.
böhm's theorem fails
in the lambda-mu-calculus.
r. david : every unsolvable lambda-terme has a decoration deco.ps
: tlca'99 (published in lncs 1581 p 98-113).
a proof of r. kerth's conjecture.
this implies the existence of uncountably many continuous (or stable)
graph models with distinct theories.
r.david & k.nour : a syntactical
proof of the operational equivalence of two lambda-terms i=j.ps
. notes aux cras 1997.
we give an elementary
(and purely arithmetical) proof of the fact that i and j (its infinite
eta-expansion) are operationaly equivalent.
r.david : the inf function in
the system f
inf_tcs.ps . tcs 1994.
i give an algorithm
(typable of the good type in system f) that computes the minimum of two
church numerals in time o(min. log(min)). this is the best known
algorithm.
r.david : un algorithme primitif
recursif pour la fonction inf
inf_cras.ps note aux cras 1994.
i give a primitive recursive
algorithm (using lists) that computes the minimum of two integers in
time o(min).
r.david : une preuve simple de résultats classiques en lambda calcul. note aux cras 1995 preuves.pdf
i
give simple proofs of the standardization theorem, the theorem of
finiteness of developments and the church rosser property of the lambda
calculus.
.
thèses
encadrées et disponibles
b.guillaume : un
calcul de substitutions avec étiquettes guillaume.ps
g. mounier : un
lambda calcul intuitioniste avec exceptions
mounier.ps
w. py :
confluence en lambda mu calcul py.pdf
y. bertini : la notion d'indéfini en lambda calcul
bertini.pdf
p. thévenon : vers un assistant à la preuve en langue naturelle thevenon.pdf
page d'accueil
du lama
bienvenue sur ma page personnelle Précédent 69 Précédent 68 Précédent 67 Précédent 66 Précédent 65 Précédent 64 Précédent 63 Précédent 62 Précédent 61 Précédent 60 Précédent 59 Précédent 58 Précédent 57 Précédent 56 Précédent 55 Précédent 54 Précédent 53 Précédent 52 Précédent 51 Précédent 50 Précédent 49 Précédent 48 Précédent 47 Précédent 46 Précédent 45 Précédent 44 Précédent 43 Précédent 42 Précédent 41 Précédent 40 Suivant 71 Suivant 72 Suivant 73 Suivant 74 Suivant 75 Suivant 76 Suivant 77 Suivant 78 Suivant 79 Suivant 80 Suivant 81 Suivant 82 Suivant 83 Suivant 84 Suivant 85 Suivant 86 Suivant 87 Suivant 88 Suivant 89 Suivant 90 Suivant 91 Suivant 92 Suivant 93 Suivant 94 Suivant 95 Suivant 96 Suivant 97 Suivant 98 Suivant 99 Suivant 100