14 found
Order:
  1.  27
    René David & Karim Nour (2003). A Short Proof of the Strong Normalization of Classical Natural Deduction with Disjunction. Journal of Symbolic Logic 68 (4):1277-1288.
    We give a direct, purely arithmetical and elementary proof of the strong normalization of the cut-elimination procedure for full (i.e., in presence of all the usual connectives) classical natural deduction.
    Direct download (9 more)  
     
    Export citation  
     
    My bibliography   5 citations  
  2.  36
    René David & Karim Nour (1995). Storage Operators and Directed Lambda-Calculus. Journal of Symbolic Logic 60 (4):1054-1086.
    Storage operators have been introduced by J. L. Krivine in [5] they are closed λ-terms which, for a data type, allow one to simulate a "call by value" while using the "call by name" strategy. In this paper, we introduce the directed λ-calculus and show that it has the usual properties of the ordinary λ-calculus. With this calculus we get an equivalent--and simple--definition of the storage operators that allows to show some of their properties: $\bullet$ the stability of the set (...)
    Direct download (8 more)  
     
    Export citation  
     
    My bibliography  
  3.  35
    Rene David & Walter Py (2001). $Lambdamu$-Calculus and Bohm's Theorem. Journal of Symbolic Logic 66 (1):407-413.
    The $\lambda\mu$-calculus is an extension of the $\lambda$-calculus that has been introduced by M Parigot to give an algorithmic content to classical proofs. We show that Bohm's theorem fails in this calculus.
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  4.  5
    René David (2001). Normalization Without Reducibility. Annals of Pure and Applied Logic 107 (1-3):121-130.
    In [gallier], general results (due to Coppo, Dezani and Veneri) relating properties of pure lambda terms and their typability in some systems with conjunctive types are proved in a uniform way by using the reducibility method.This paper gives a very short proof of the same results (actually, one of them is a bit stronger) using purely arithmetical methods.
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography   3 citations  
  5.  7
    René David (1982). A Very Absolute Pi-1-2 Real Singleton. Annals of Mathematical Logic 23 (2-3):101-120.
    I give a class forcing that adds a real which is Pi-1-2 and for which no forcing extension (by a set of conditions) can destroy this definability.
    No categories
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography   5 citations  
  6.  3
    René David (1982). Δ31 Reals. Annals of Mathematical Logic 23 (2-3):121-125.
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography   3 citations  
  7.  14
    René David & Walter Py (2001). -Calculus and Böhm's Theorem. Journal of Symbolic Logic 66 (1):407-413.
    The λμ-calculus is an extension of the λ-calculus that has been introduced by M Parigot to give an algorithmic content to classical proofs. We show that Bohm's theorem fails in this calculus.
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  8.  9
    René David & Marek Zaionc (2009). Counting Proofs in Propositional Logic. Archive for Mathematical Logic 48 (2):185-199.
    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.
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography  
  9.  4
    René David & Karim Nour (2010). Strong Normalization Results by Translation. Annals of Pure and Applied Logic 161 (9):1171-1179.
    We prove the strong normalization of full classical natural deduction by using a translation into the simply typed λμ-calculus. We also extend Mendler’s result on recursive equations to this system.
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography  
  10.  4
    René David (1980). A Result of Relative Consistency About the Predicate WO(Δ, Κ). Journal of Symbolic Logic 45 (3):483-492.
    Direct download (7 more)  
     
    Export citation  
     
    My bibliography  
  11.  1
    René David (2004). Domains and Lambda-Calculi. Bulletin of Symbolic Logic 10 (2):211-213.
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  12. R. Amadio, P. L. Curien & Rene David (2004). REVIEWS-Domains and Lambda-Calculi. Bulletin of Symbolic Logic 10 (2):211-212.
     
    Export citation  
     
    My bibliography  
  13. René David (1987). McAloon Kenneth. On the Sequence of Models HODn. Fundamenta Mathematicae, Vol. 82 , Pp. 85–93.Jech Thomas J.. Forcing with Trees and Ordinal Definability. Annals of Mathematical Logic, Vol. 7 No. 4 , Pp. 387–409.Zadrożny Włodzimierz. Iterating Ordinal Definability. Annals of Pure and Applied Logic, Vol. 24 , Pp. 263–310. [REVIEW] Journal of Symbolic Logic 52 (2):570-571.
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  14. Rene David (1987). Review: Kenneth McAloon, On the Sequence of Models $Operatorname{HOD}_n$; Thomas J. Jech, Forcing with Trees and Ordinal Definability; Wlodzimierz Zadrozny, Iterating Ordinal Definability. [REVIEW] Journal of Symbolic Logic 52 (2):570-571.