Improving Type Error Messages in OCaml

Autor: Arthur Charguéraud

Publikováno v: Electronic Proceedings in Theoretical Computer Science, Vol 198, Iss Proc. ML/OCaml 2014, Pp 80-97 (2015)

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: https://doaj.org/article/670ae6144441483b9bb9fbe95b41cd11

An AST for Representing Programs with Invariants and Proofs

Autor: Guillaume Bertholon, Arthur Charguéraud

Publikováno v: Journées Francophones des Langages Applicatifs
JFLA 2023-34èmes Journées Francophones des Langages Applicatifs
JFLA 2023-34èmes Journées Francophones des Langages Applicatifs, Jan 2023, Praz-sur-Arly, France. pp.43-58
HAL

National audience; Deductive verification enables one to check that a program satisfies its specification. There are mainly two approaches: either the user provides invariants in the form of annotations and use a tool to extract proof obligations, li

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::08535ba18d69bdd404e2cd6993ef9ff1
https://inria.hal.science/hal-03936618

Specification and Verification of a Transient Stack

Autor: Alexandre Moine, Arthur Charguéraud, François Pottier

Publikováno v: CPP 2022-11th ACM SIGPLAN International Conference on Certified Programs and Proofs
CPP 2022-11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2022, Philadelphia, United States. ⟨10.1145/3497775.3503677⟩

International audience; A transient data structure is a package of an ephemeral data structure, a persistent data structure, and fast conversions between them. We describe the specification and proof of a transient stack and its iterators. This data

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::4ec834bd1adabfaa65bce2b975b82fb0
https://hal.inria.fr/hal-03472028

Omnisemantics: Smooth Handling of Nondeterminism

Autor: Arthur Charguéraud, Adam Chlipala, Andres Erbsen, Samuel Gruetter

This article gives an in-depth presentation of the omni-big-step and omni-small-step styles of semantic judgments. These styles describe operational semantics by relating starting states to sets of outcomes rather than to individual outcomes. A singl

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::7fbed6d35089744fd04b242b07004f87
https://hal.inria.fr/hal-03255472v3

Provably and practically efficient granularity control

Autor: Umut A. Acar, Vitaly Aksenov, Mike Rainey, Arthur Charguéraud

Publikováno v: PPoPP
PPoPP 2019-Principles and Practice of Parallel Programming
PPoPP 2019-Principles and Practice of Parallel Programming, Feb 2019, Washington DC, United States. ⟨10.1145/3293883.3295725⟩

International audience; Over the past decade, many programming languages and systems for parallel-computing have been developed, e.g., Fork/Join and Habanero Java, Parallel Haskell, Parallel ML, and X10. Although these systems raise the level of abst

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::384ea3114522d00696d2efe3dfe8dcec
https://doi.org/10.1145/3293883.3295725