3 papers
math.LO2023
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…
math.LO2017
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…
math.LO2017
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…