Environmental Bisimulations for Probabilistic Higher-order Languages

Autor: Valeria Vignudelli, Davide Sangiorgi

Publikováno v: POPL '16
POPL '16, Jan 2016, St. Petersburg, United States. ⟨10.1145/2837614.2837651⟩
POPL

Environmental bisimulations for probabilistic higher-order languages are studied. In contrast with applicative bisimulations, environmental bisimulations are known to be more robust and do not require sophisticated techniques such as Howe’s in the

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::33b1c3e4ba484a583d8e30122f794de5
https://doi.org/10.1145/3350618

Caractérisation impérative des algorithmes séquentiels en temps quelconque, primitif récursif ou polynomial

Autor: Marquer, Yoann

Les résultats de Colson ou de Moschovakis remettent en question que le modèle récursif primitif puisse calculer une valeur par tous les moyens possibles : il y a toutes les fonctions voulues mais il manque des algorithmes. La thèse de Church expr

Externí odkaz: http://www.theses.fr/2015PESC1121/document

Complexity Information Flow in a Multi-threaded Imperative Language

Autor: Romain Péchoux, Jean-Yves Marion

Publikováno v: [Research Report] 2012, pp.16
TAMC 2014
TAMC 2014, Apr 2014, Chennai, India. pp.124-140, ⟨10.1007/978-3-319-06089-7_9⟩
Lecture Notes in Computer Science ISBN: 9783319060880
TAMC
HAL

International audience; We propose a type system to analyze the time consumed by multi-threaded imperative programs with a shared global memory, which delineates a class of safe multi-threaded programs. We demon-strate that a safe multi-threaded prog

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::0dbd4e9f43c8d814774094647eb6696e
https://inria.hal.science/hal-00684026/file/hulotte.pdf

Sémantiques formelles

Autor: Blazy, Sandrine

Publikováno v: Informatique [cs]. Université d'Evry-Val d'Essonne, 2008

Ce mémoire présente plusieurs définitions de sémantiques formelles et de transformations de programmes, et expose les choix de conception associés. En particulier, ce mémoire décrit une transformation de programmes inspirée de l'évaluation p

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::e286a3d4efa64d3cf9de06dbd6d7c233
https://theses.hal.science/tel-00336576

Separation Logic for Small-step Cminor

Autor: Andrew W. Appel, Sandrine Blazy

Publikováno v: 20th Int. Conference on Theorem Proving in Higher Order Logics (TPHOLs 2007)
20th Int. Conference on Theorem Proving in Higher Order Logics (TPHOLs 2007), Sep 2007, Kaiserslautern, Germany. pp.5-21
Lecture Notes in Computer Science ISBN: 9783540745907
TPHOLs

Cminor is a mid-level imperative programming language; there are proved-correct optimizing compilers from C to Cminor and from Cminor to machine language. We have redesigned Cminor so that it is suitable for Hoare Logic reasoning and we have designed

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::3391e909f66c097a2a20ca035c7c2e09
https://hal.inria.fr/inria-00165915