CCL

Összesen 4 találat.
#/oldal:
Részletezés:
Rendezés:

1.

001-es BibID:BIBFORM110536
035-os BibID:(WoS)000933733600001
Első szerző:Battyányi Péter (informatikus, matematikus)
Cím:Normalization in the simply typed lambda mu mu' rho theta epsilon-calculus / Péter Battyányi, Karim Nour
Dátum:2023
ISSN:0960-1295
Megjegyzések:In this paper, in connection with the program of extending the Curry-Howard isomorphism to classical logic, we study the lambda mu-calculus of Parigot emphasizing the difference between the original version of Parigot and the version of de Groote in terms of normalization properties. In order to talk about a satisfactory representation of the integers, besides the usual beta-, mu-, and mu'-reductions, we consider the lambda mu-calculus augmented with the reduction rules rho,theta and epsilon. We show that we need all of these rules for this purpose. Then we prove that, with the syntax of Parigot, the calculus enjoys the strong normalization property even when we add the rules rho,theta, and epsilon, while the lambda mu-calculus presented with the more flexible de Groote-style syntax, in contrast, has only the weak normalization property. In particular, we present a normalization algorithm for the beta mu mu 0 theta epsilon-reduction in the de Groote-style calculus.
Tárgyszavak:Természettudományok Matematika- és számítástudományok idegen nyelvű folyóiratközlemény külföldi lapban
folyóiratcikk
lambda mu-calculus
classical logic
strong normalization
weak normalization
normalization algorithm
Megjelenés:Mathematical Structures In Computer Science. - 32 : 8 (2023), p. 1066-1098. -
További szerzők:Karim, Nour
Internet cím:Szerző által megadott URL
DOI
Intézményi repozitóriumban (DEA) tárolt változat
Borító:

2.

001-es BibID:BIBFORM094048
035-os BibID:(cikkazonosító)17 (WoS)000439433300004 (Scopus)85055852173
Első szerző:Battyányi Péter (informatikus, matematikus)
Cím:An estimation for the lengths of reduction sequences of the lambda mu rho theta-calculus / Péter Battyányi, Karim Nour
Dátum:2018
ISSN:1860-5974
Tárgyszavak:Természettudományok Matematika- és számítástudományok idegen nyelvű folyóiratközlemény külföldi lapban
folyóiratcikk
Megjelenés:Logical Methods in Computer Science. - 14 : 2 (2018), p. 1-35. -
További szerzők:Karim, Nour
Internet cím:DOI
Szerző által megadott URL
Intézményi repozitóriumban (DEA) tárolt változat
Borító:

3.

001-es BibID:BIBFORM094046
035-os BibID:(WoS)000532484000059 (Scopus)85088010956
Első szerző:Battyányi Péter (informatikus, matematikus)
Cím:Normalization proofs for the un-typed mu mu'-calculus / Péter Battyányi, Karim Nour
Dátum:2020
ISSN:2473-6988
Tárgyszavak:Természettudományok Matematika- és számítástudományok idegen nyelvű folyóiratközlemény külföldi lapban
folyóiratcikk
Megjelenés:AIMS Mathematics. - 5 : 4 (2020), p. 3702-3713. -
További szerzők:Karim, Nour
Internet cím:Szerző által megadott URL
DOI
Intézményi repozitóriumban (DEA) tárolt változat
Borító:

4.

001-es BibID:BIBFORM079630
035-os BibID:(cikkazonosító)34 (WoS)000419163000035 (Scopus)85041809580
Első szerző:Battyányi Péter (informatikus, matematikus)
Cím:Strong normalization of lambda-Sym-Prop- and lambda-bar-mu-mu-tilde-star- calculi / Péter Battyányi, Karim Nour
Dátum:2017
ISSN:1860-5974
Megjegyzések: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 of classical propositional logic in natural deduction style. Then we give a translation between the lambda-Sym-Prop-calculus and the lambda-bar-mu-mu-tilde-star-calculus, which is the implicational part of the lambda-bar-mu-mu-tilde-calculus invented by Curien and Herbelin [3] extended with negation. In this paper we adapt the method of David and Nour [4] for proving strong normalization. The novelty in our proof is the notion of zoom-in sequences of redexes, which leads us directly to the proof of the main theorem.
Tárgyszavak:Műszaki tudományok Informatikai tudományok idegen nyelvű folyóiratközlemény külföldi lapban
folyóiratcikk
arithmetical proof
strong normalization
classical logic
zoom-in sequences of redexes
Megjelenés:Logical Methods in Computer Science. - 13 : 3 (2017), p. 1-22. -
További szerzők:Karim, Nour
Internet cím:Szerző által megadott URL
DOI
Intézményi repozitóriumban (DEA) tárolt változat
Borító:
Rekordok letöltése1