13 found
Sort by:
  1. René David & Karim Nour (2010). Strong Normalization Results by Translation. Annals of Pure and Applied Logic 161 (9):1171-1179.
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  2. 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.
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  3. R. Amadio, P. L. Curien & Rene David (2004). REVIEWS-Domains and Lambda-Calculi. Bulletin of Symbolic Logic 10 (2):211-212.
    No categories
     
    My bibliography  
     
    Export citation  
  4. René David (2004). Domains and Lambda-Calculi. Bulletin of Symbolic Logic 10 (2):211-213.
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation  
  5. 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 (8 more)  
     
    My bibliography  
     
    Export citation  
  6. 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)  
     
    My bibliography  
     
    Export citation  
  7. 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 (4 more)  
     
    My bibliography  
     
    Export citation  
  8. 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)  
     
    My bibliography  
     
    Export citation  
  9. 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 (7 more)  
     
    My bibliography  
     
    Export citation  
  10. 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.
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  11. 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)  
     
    My bibliography  
     
    Export citation  
  12. René David (1982). Δ31 Reals. Annals of Mathematical Logic 23 (2-3):121-125.
    No categories
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  13. René David (1980). A Result of Relative Consistency About the Predicate WO(Δ, Κ). Journal of Symbolic Logic 45 (3):483-492.
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation