6 citations · 17 across the 27 of their papers we have counts for
29 papers
Normalization properties of -calculus using realizability semantics
Peter Battyanyi, Karim Nour
In this paper, we present a general realizability semantics for the simply typed -calculus. Then, based on this semantics, we derive both weak and strong normalization results…
Strong normalization of lambda-Sym-Prop- and lambda-bar-mu-mu-tilde-star- calculi
Peter Battyanyi, Karim Nour
In this paper we give an arithmetical proof of the strong normalization of lambda-Sym-Prop of Berardi and Barbanera [1], which can be considered as a formulae-as-types translation…
An estimation for the lengths of reduction sequences of the -calculus
Péter Battyányi, Karim Nour
Since it was realized that the Curry-Howard isomorphism can be extended to the case of classical logic as well, several calculi have appeared as candidates for the encodings of pro…
A revised completeness result for the simply typed -calculus using realizability semantics
Karim Nour, Mohamad Ziadeh
In this paper, we define a new realizability semantics for the simply typed lambda-mu-calculus. We show that if a term is typable, then it inhabits the interpretation of its type.…
About the range property for H
René David, Karim Nour
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 infinite cardinality.
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…