Operational semantics for LYaPAS
Prikladnaya Diskretnaya Matematika. Supplement, no. 8 (2015), pp. 131-132
Cet article a éte moissonné depuis la source Math-Net.Ru
The development of the operational semantics for LYaPAS is considered. The following two applications are possible: the proof of the complex-element references correctness by abstract interpretation method and the creation of a certified compiler.
Keywords:
operational semantics, abstract interpretation, certified compiler.
Mots-clés : LYaPAS
Mots-clés : LYaPAS
@article{PDMA_2015_8_a49,
author = {A. O. Zhukovskaja and D. A. Stefantsov},
title = {Operational semantics for {LYaPAS}},
journal = {Prikladnaya Diskretnaya Matematika. Supplement},
pages = {131--132},
year = {2015},
number = {8},
language = {ru},
url = {http://geodesic.mathdoc.fr/item/PDMA_2015_8_a49/}
}
A. O. Zhukovskaja; D. A. Stefantsov. Operational semantics for LYaPAS. Prikladnaya Diskretnaya Matematika. Supplement, no. 8 (2015), pp. 131-132. http://geodesic.mathdoc.fr/item/PDMA_2015_8_a49/
[1] Agibalov G. P., Lipskii V. B., Pankratova I. A., “O kriptograficheskom rasshirenii i ego realizatsii dlya Russkogo yazyka programmirovaniya”, Prikladnaya diskretnaya matematika, 2013, no. 3, 93–104
[2] Besson F., Cachera D., Jensen T., Pichardie D., “Certified static analysis by abstract interpretation”, Foundations of Security Analysis and Design, LNCS, 5705, 2009, 223–257 | Zbl
[3] The CompCert page, http://compcert.inria.fr/
[4] The Coq Proof Assistant page, https://coq.inria.fr/