Skip to content

Commit ad6bcb5

Browse files
authored
Add 4 papers (#2872)
Unboxed Data Constructors: Or, How cpp Decides a Halting Problem A practical mode system for recursive definitions Merlin: a language server for OCaml (experience report) Tail Modulo Cons, OCaml, and Relational Separation Logic
1 parent 9eca09c commit ad6bcb5

File tree

1 file changed

+131
-0
lines changed

1 file changed

+131
-0
lines changed

data/papers.yml

Lines changed: 131 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1393,3 +1393,134 @@ papers:
13931393
- description: "Read Online"
13941394
uri: https://icfp23.sigplan.org/details/ocaml-2023-papers/13/Wasocaml-a-compiler-from-OCaml-to-WebAssembly
13951395
featured: false
1396+
- title: "Unboxed Data Constructors: Or, How cpp Decides a Halting Problem"
1397+
publication: International Conference on Functional Programming (ICFP)
1398+
abstract: >
1399+
We propose a new language feature for ML-family languages, the ability to
1400+
selectively unbox certain data constructors, so that their runtime
1401+
representation gets compiled away to just the identity on their argument.
1402+
Unboxing must be statically rejected when it could introduce confusion,
1403+
that is, distinct values with the same representation. We discuss the
1404+
use-case of big numbers, where unboxing allows to write code that is both
1405+
efficient and safe, replacing either a safe but slow version or a fast
1406+
but unsafe version. We explain the static analysis necessary to reject
1407+
incorrect unboxing requests. We present our prototype implementation of
1408+
this feature for the OCaml programming language, discuss several design
1409+
choices and the interaction with advanced features such as Guarded
1410+
Algebraic Datatypes. Our static analysis requires expanding type
1411+
definitions in type expressions, which is not necessarily normalizing in
1412+
presence of recursive type definitions. In other words, we must decide
1413+
normalization of terms in the first-order λ-calculus with recursion. We
1414+
provide an algorithm to detect non-termination on-the-fly during
1415+
reduction, with proofs of correctness and completeness. Our algorithm
1416+
turns out to be closely related to the normalization strategy for macro
1417+
expansion in the cpp preprocessor.
1418+
authors:
1419+
- Nicolas Chataing
1420+
- Stephen Dolan
1421+
- Gabriel Scherer
1422+
- Jeremy Yallop
1423+
tags:
1424+
- icfp
1425+
year: 2023
1426+
links:
1427+
- description: "Read Online"
1428+
uri: https://dl.acm.org/doi/10.1145/3632893
1429+
featured: false
1430+
- title: "A practical mode system for recursive definitions"
1431+
publication: Principles of Programming Languages (POPL)
1432+
abstract: >
1433+
In call-by-value languages, some mutually-recursive definitions can be
1434+
safely evaluated to build recursive functions or cyclic data structures,
1435+
but some definitions (let rec x = x + 1) contain vicious circles and
1436+
their evaluation fails at runtime. We propose a new static analysis to
1437+
check the absence of such runtime failures. We present a set of
1438+
declarative inference rules, prove its soundness with respect to the
1439+
reference source-level semantics of Nordlander, Carlsson, and Gill
1440+
[2008], and show that it can be directed into an algorithmic backwards
1441+
analysis check in a surprisingly simple way. Our implementation of this
1442+
new check replaced the existing check used by the OCaml programming
1443+
language, a fragile syntactic criterion which let several subtle bugs
1444+
slip through as the language kept evolving. We document some issues that
1445+
arise when advanced features of a real-world functional language
1446+
(exceptions in first-class modules, GADTs, etc.) interact with safety
1447+
checking for recursive definitions.
1448+
authors:
1449+
- Alban Reynaud
1450+
- Gabriel Scherer
1451+
- Jeremy Yallop
1452+
tags:
1453+
- popl
1454+
year: 2021
1455+
links:
1456+
- description: "Read Online"
1457+
uri: https://dl.acm.org/doi/10.1145/3434326
1458+
featured: false
1459+
- title: "Merlin: A Language Server for OCaml (Experience Report)"
1460+
publication: International Conference on Functional Programming (ICFP)
1461+
abstract: >
1462+
We report on the experience of developing Merlin, a language server for
1463+
the OCaml programming language in development since 2013. Merlin is a
1464+
daemon that connects to your favourite text editor and provides services
1465+
that require a fine-grained understanding of the programming language
1466+
syntax and static semantics: instant feedback on warnings and errors,
1467+
autocompletion, 'type of the code under the cursor', 'go to definition',
1468+
etc. Language servers need to handle incomplete and partially-incorrect
1469+
programs, and try to be incremental to minimize recomputation after small
1470+
editing actions. Merlin was built by carefully adapting the existing tools
1471+
(the OCamllex lexer and Menhir parser generators) to better support
1472+
incrementality, incompleteness and error handling. These extensions are
1473+
elegant and general, as demonstrated by the interesting, unplanned uses
1474+
that the OCaml community found for them. They could be adapted to other
1475+
frontends -- in any language. Besides incrementality, we discuss the way
1476+
Merlin communicates with editors, describe the design decisions that went
1477+
into some demanding features and report on some of the non-apparent
1478+
difficulties in building good editor support, emerging from expressive
1479+
programming languages or frustrating tooling ecosystems. We expect this
1480+
experience report to be of interest to authors of interactive language
1481+
tooling for any programming language; many design choices may be reused,
1482+
and some hard-won lessons can serve as warnings.
1483+
authors:
1484+
- Frédéric Bour
1485+
- Thomas Refis
1486+
- Gabriel Scherer
1487+
tags:
1488+
- icfp
1489+
year: 2018
1490+
links:
1491+
- description: "Read Online"
1492+
uri: https://dl.acm.org/doi/10.1145/3236798
1493+
featured: false
1494+
- title: "Tail Modulo Cons, OCaml, and Relational Separation Logic"
1495+
publication: Principles of Programming Languages (POPL)
1496+
abstract: >
1497+
Common functional languages incentivize tail-recursive functions, as
1498+
opposed to general recursive functions that consume stack space and may
1499+
not scale to large inputs. This distinction occasionally requires writing
1500+
functions in a tail-recursive style that may be more complex and slower
1501+
than the natural, non-tail-recursive definition. This work describes our
1502+
implementation of the tail modulo constructor (TMC) transformation in the
1503+
OCaml compiler, an optimization that provides stack-efficiency for a
1504+
larger class of functions—tail-recursive modulo constructors—which
1505+
includes in particular the natural definition of `List.map` and many
1506+
similar recursive data-constructing functions. We prove the correctness
1507+
of this program transformation in a simplified setting—a small untyped
1508+
calculus—that captures the salient aspects of the OCaml implementation.
1509+
Our proof is mechanized in the Coq proof assistant, using the Iris base
1510+
logic. An independent contribution of our work is an extension of the
1511+
Simuliris approach to define simulation relations that support different
1512+
calling conventions. To our knowledge, this is the first use of Simuliris
1513+
to prove the correctness of a compiler transformation.
1514+
authors:
1515+
- Clément Allain
1516+
- Frédéric Bour
1517+
- Basile Clément
1518+
- François Pottier
1519+
- Gabriel Scherer
1520+
tags:
1521+
- popl
1522+
year: 2025
1523+
links:
1524+
- description: "Read Online"
1525+
uri: https://arxiv.org/abs/2411.19397
1526+
featured: false

0 commit comments

Comments
 (0)