Geodesic
IMP with exceptions over decorated logic
Discrete mathematics & theoretical computer science, Tome 20 (2018) no. 2.

Voir la notice de l'article provenant de la source Episciences

In this paper, we facilitate the reasoning about impure programming languages, by annotating terms with “decorations”that describe what computational (side) effect evaluation of a term may involve. In a point-free categorical language,called the “decorated logic”, we formalize the mutable state and the exception effects first separately, exploiting anice duality between them, and then combined. The combined decorated logic is used as the target language forthe denotational semantics of the IMP+Exc imperative programming language, and allows us to prove equivalencesbetween programs written in IMP+Exc. The combined logic is encoded in Coq, and this encoding is used to certifysome program equivalence proofs. 
@article{DMTCS_2018_20_2_a11,
     author = {Ekici , Burak},
     title = {IMP with exceptions over decorated logic},
     journal = {Discrete mathematics & theoretical computer science},
     publisher = {mathdoc},
     volume = {20},
     number = {2},
     year = {2018},
     doi = {10.23638/DMTCS-20-2-11},
     language = {en},
     url = {http://geodesic.mathdoc.fr/articles/10.23638/DMTCS-20-2-11/}
}
TY  - JOUR
AU  - Ekici , Burak
TI  - IMP with exceptions over decorated logic
JO  - Discrete mathematics & theoretical computer science
PY  - 2018
VL  - 20
IS  - 2
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/articles/10.23638/DMTCS-20-2-11/
DO  - 10.23638/DMTCS-20-2-11
LA  - en
ID  - DMTCS_2018_20_2_a11
ER  - 
%0 Journal Article
%A Ekici , Burak
%T IMP with exceptions over decorated logic
%J Discrete mathematics & theoretical computer science
%D 2018
%V 20
%N 2
%I mathdoc
%U http://geodesic.mathdoc.fr/articles/10.23638/DMTCS-20-2-11/
%R 10.23638/DMTCS-20-2-11
%G en
%F DMTCS_2018_20_2_a11
Ekici , Burak. IMP with exceptions over decorated logic. Discrete mathematics & theoretical computer science, Tome 20 (2018) no. 2. doi : 10.23638/DMTCS-20-2-11. http://geodesic.mathdoc.fr/articles/10.23638/DMTCS-20-2-11/

Cité par Sources :