output
20022009
most citedBSDEs with stochastic Lipschitz condition and quadratic PDEs in Hilbert spaces

100 citations

researchers with a paper here
collaborating institutions
Showing math.LOShow all

33 papers · 1 filter

math.LO2009

Strong normalization results by translation

René David, Karim Nour

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…

math.LO2009

A direct proof of the confluence of combinatory strong reduction

René David

I give a proof of the confluence of combinatory strong reduction that does not use the one of lambda-calculus. I also give simple and direct proofs of a standardization theorem for…

math.LO2009★ 3 cited

Realisability Semantics for Intersection Types and Expansion Variables

Fairouz Kamareddine, Karim Nour, Vincent Rahli +1

Expansion was invented at the end of the 1970s for calculating principal typings for -terms in type systems with intersection types. Expansion variables (E-variables) were inven…

math.LO2009

A complete realisability semantics for intersection types and arbitrary expansion variables

Fairouz Kamareddine, Karim Nour, Vincent Rahli +1

Expansion was introduced at the end of the 1970s for calculating principal typings for -terms in intersection type systems. Expansion variables (E-variables) were introduced at…

math.LO2009★ 2 cited

Parametric mixed sequent calculus

Karim Nour, Olivier Laurent

In this paper, we present a propositional sequent calculus containing disjoint copies of classical and intuitionistic logics. We prove a cut-elimination theorem and we establish a…

math.LO2009★ 6 cited

A short proof of the strong normalization of the simply typed -calculus

René David, Karim Nour

We give an elementary and purely arithmetical proof of the strong normalization of Parigot's simply typed -calculus.