12 papers · ranked by Valyu relevance
David Knothe, Oliver Bringmann
Verified compilers aim to guarantee that compilation preserves the observable behavior of source programs. While small-step semantics are widely used in such compilers, they are not always the most convenient framework for structural transformations such as loop optimizations. This paper proposes an approach that…
Roberto M. Amadio
| | Preface | 7 | |---|-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|----------------------------------------| | |…
Haoxuan Yin, Andrzej S. Murawski, C. -H. Luke Ong
MetaML-style metaprogramming languages allow programmers to construct, manipulate and run code. In the presence of higherorder references for code, ensuring type safety is challenging, as free variables can escape their binders. In this paper, we present Layered Modal ML (LMML), the first metaprogramming language that…
Moida Praneeth Jain, Venkatesh Choppella
Misconceptions about program execution hinder many novice programmers. We introduce SimpliPy, a notional machine designed around a carefully chosen Python subset to clarify core control flow and scoping concepts. Its foundation is a precise operational semantics that explicitly tracks source code line numbers for each…
Christian Antić
A systematic algebraic framework for composing and decomposing logic programs is currently missing, limiting our ability to analyze and construct programs in a modular way. In this paper, we introduce set-like operations for (propositional Horn) logic programs that allow for a structured manipulation of rule bodies.…
Thomas Bagrel
La programmation par passage de destination introduit le concept de destination, qui représente l'adresse d'une cellule mémoire encore vierge sur laquelle on ne peut écrire qu'une fois. Ces destinations peuvent être passées en tant que paramètres de fonction, permettant à l'appelant de garder le contrôle de la gestion…
Jun Tan, Guannan Wei
Multi-stage programming with quotations has long provided a powerful way to generate and manipulate code. By treating code as data, programmers can write multi-stage programs in which earlier stages produce specialized code from inputs available at generation time. Modern typed multi-stage languages (e.g., MetaML…
Narges Khakpour, Nicolas Berthier
We introduce a scalable, modular, and sound approach for automatically constructing formal security specifications for Java bytecode programs in the form of method summaries. A summary provides an abstract representation of a method's security behavior, consisting of the conditions under which the method can be…
Zichen Zhang, Simon Oddershede Gregersen, Joseph Tassarotti
One strategy for reasoning about programs that have certain kinds of effects is to use program logics that provide specialized rules for reasoning about these effects. However, developing program logics requires skills that are distinct from those needed for using program logics, making the development of new logics…
Stephen Mell, Zdancewic, Steve, Bastani + 1 more
We consider the problem of synthesizing programs with numerical constants that optimize a quantitative objective, such as accuracy, over a set of input-output examples. We propose a general framework for optimal synthesis of such programs in a given domain specific language (DSL), with provable optimality guarantees.…
Michael Lee, Ningning Xie, Oleg Kiselyov, Jeremy Yallop
Metaprogramming and effect handlers interact in unexpected, and sometimes undesirable, ways. One example is scope extrusion: the generation of ill-scoped code. Scope extrusion can either be preemptively prevented, via static type systems, or retroactively detected, via dynamic checks. Static type systems exist in…
Attila Egri-Nagy
Programming languages tend to evolve over time to use more and more concepts from theoretical computer science. Still, there is a gap between programming and pure mathematics. Not all theoretical results have realized their promising applications. The algebraic decomposition of finite state automata (Krohn-Rhodes…