René David

(dernière mise à jour : 24/01/2014)




                                       René David                                                                                                

                                                      In my office                                                                                     Outside my office

My position

I am now retired and I do not work any more in lambda calculus.
I am now involved in mountain for handicapped persons. My mail address at the university is no more valid but you can reach me by contacting one of my ex-colleages (Karim, Christophe, Pierre, ...)


Below are files that you can download



**********************************************************************************************************************


Conférences

"Peut-on faire des mathématiques avec un ordinateur"    Le fichier associé est un fichier pdf.


"Peut-on avoir confiance en l'informatique ?"   Le fichier associé est un fichier pdf.

Meetings I have organized


Publications about teaching

Publications in proof theory and lambda-calculus


  • R David, C Raffalli, G Theyssier, K Grygiel, J Kozik, M Zaionc :  Some properties of random lambda-terms.   We present quantitative analysis of various (syntactic and behavioral) properties of random   lambda-terms. Our main results are that asymptotically all the terms are strongly normalizing and that any fixed closed term almost never appears in a random term.  Surprisingly, in combinatory logic (the translation of the lambda-calculus into combinators) the result is exactly opposite. We show that almost all terms are  not strongly normalizing. This due to the fact that any fixed combinator almost always appears in a random combinator. LMCS Vol 9, Issue 1, 2013.  lcount.pdf

  • R. David & K. Nour : About the range property for H. Recently, A. Polonsky  has shown that the range property fails for H. We give here some conditions on a closed term that imply that its range has an infnite cardinality. range.pdf   LMCS, Vol 10, Issue 2, 2014, p 1-18

  • R. David : A short proof that adding some permutation rules to beta preserves SN. I show that, if a term is SN for beta, it remains SN when some permutation rules are added. TCS, Vol 412, Issue 11, March 2011, p 1022-1026 assoc.pdf

  • R. David & M. Zaionc : Counting proofs in propositional logic. We give a procedure for counting the number of different proofs of a formula in various sorts of propositional logic. This number is either an integer (that may be 0 if the formula is not provable) or infinite. Archive for Mathematical Logic (2009) 48:185-199. counting_proofs.pdf

  • R. David & K. Nour : Strong normalization results by translation. We prove the strong normalization of full classical natural deduction (i.e. with conjunction, disjunction and permutative conversions) by using a translation into the simply typed lambda-mu-calculus. We also extend Mendler's result on recursive equations to this system. APAL, Vol 161, Issue 9, June 2010, p 1171-1179 translation.pdf

  • R. David : I give a proof of the confluence of combinatory strong reduction that does not use the one of lambda-calculus. This problem appeared as #1 in the TLCA list of open problems. I also give simple and direct proofs of a standardization theorem for this reduction and the strong normalization of simply typed terms.  TCS 410/42 pp 4204-4215 (2009). confluence.pdf

  • 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.
    • .

    Phd thesis of Chambéry students 

    Publications in set theory 

    Page d'accueil du LAMA