Zobrazeno 1 - 10
of 53
pro vyhledávání: '"Charguéraud, Arthur"'
In this paper, we propose an empirical method for evaluating the performance of parallel code. Our method is based on a simple idea that is surprisingly effective in helping to identify causes of poor performance, such as high parallelization overhea
Externí odkaz:
http://arxiv.org/abs/1709.03767
Autor:
Charguéraud, Arthur
Publikováno v:
EPTCS 198, 2015, pp. 80-97
Cryptic type error messages are a major obstacle to learning OCaml or other ML-based languages. In many cases, error messages cannot be interpreted without a sufficiently-precise model of the type inference algorithm. The problem of improving type er
Externí odkaz:
http://arxiv.org/abs/1512.01897
Autor:
CHARGUÉRAUD, ARTHUR1 arthur.chargueraud@inria.fr, CHLIPALA, ADAM2 adamc@csail.mit.edu, ERBSEN, ANDRES2 andreser@mit.edu, GRUETTER, SAMUEL2 gruetter@mit.edu
Publikováno v:
ACM Transactions on Programming Languages & Systems. Mar2023, Vol. 45 Issue 1, p1-43. 43p.
Publikováno v:
ARRAY 2023-Workshop-PLDI 2023
ARRAY 2023-Workshop-PLDI 2023, Jun 2023, Orlando (Florida), United States.
ARRAY 2023-Workshop-PLDI 2023, Jun 2023, Orlando (Florida), United States.
International audience; We present OptiTrust, an interactive framework for optimizing general-purpose C code via series of programmer-guided, source-to-source transformations. Optimization steps are described in transformation scripts, expressed as O
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=od_______165::e017aa96028b49fa00948376346d9fcd
https://inria.hal.science/hal-04053772/document
https://inria.hal.science/hal-04053772/document
Autor:
Charguéraud, Arthur
Publikováno v:
Computer Science [cs]. Université de Strasbourg, 2023
Separation Logic brought a major breakthrough in the area of program verification. Since its introduction, Separation Logic has made its way into a number of practical tools that are used on a daily basis for verifying programs, ranging from operatin
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=od_______165::5e67546e83ef2496488389eb8914712f
https://inria.hal.science/tel-04076725/file/chargueraud_hdr.pdf
https://inria.hal.science/tel-04076725/file/chargueraud_hdr.pdf
Autor:
Charguéraud, Arthur
Publikováno v:
Proceedings of the ACM on Programming Languages
Proceedings of the ACM on Programming Languages, ACM, 2020, 4, ⟨10.1145/3408998⟩
Proceedings of the ACM on Programming Languages, 2020, 4, ⟨10.1145/3408998⟩
Proceedings of the ACM on Programming Languages, ACM, 2020, 4, ⟨10.1145/3408998⟩
Proceedings of the ACM on Programming Languages, 2020, 4, ⟨10.1145/3408998⟩
International audience; This paper presents a simple mechanized formalization of Separation Logic for sequential programs. This formalization is aimed for teaching the ideas of Separation Logic, including its soundness proof and its recent enhancemen
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::455efdd38c4ffe63bb364cdc8f509879
https://hal.inria.fr/hal-03108936/document
https://hal.inria.fr/hal-03108936/document
This paper introduces the CPS-big-step and CPS-small-step judgments. These two judgments describe operational semantics by relating starting states to sets of outcomes rather than to individual outcomes. A single derivation of these semantics for a p
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::799dbd8869ce40c200d44d83b524b314
https://hal.inria.fr/hal-03255472
https://hal.inria.fr/hal-03255472
Publikováno v:
2021, ⟨swh:1:dir:80952d7602e8e9614979f1b1f50fdad8a4c369f1;origin=https://hal.archives-ouvertes.fr/hal-03473197;visit=swh:1:snp:781fc4f58efbdfa6ea16006272793bf7c610d760;anchor=swh:1:rel:3df60f40567bfdf2b365cac2fe61c6bb38d94503;path=/⟩
This repository contains the formalization of a transient stack and its iterator, as described in the CPP'22 paper "Specification and Verification of a Transient Stack".
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=od______1398::d9e2e22997c65ddcea29b39ef9e95f16
https://hal.inria.fr/hal-03473197
https://hal.inria.fr/hal-03473197
Akademický článek
Tento výsledek nelze pro nepřihlášené uživatele zobrazit.
K zobrazení výsledku je třeba se přihlásit.
K zobrazení výsledku je třeba se přihlásit.