Constraint Programming (CP) is a declarative paradigm where a programmer models a problem in terms of constraints over some set of variables. Monadic Constraint Programming (MCP) integrates CP with functional programming by modeling the constraint solver as a monad threaded through a monadic search tree. This abstraction allows us to define search as a first-class object which can be constructed from composable search transformers. We introduce Effectful Constraint Programming (ECP), a re-imagining of monadic constraint programming using the increasingly-popular framework of algebraic effects and handlers. To overcome the performance drawbacks of effects, we use multi-stage programming to generate efficient search procedures from high-level, abstract descriptions.
Structural operational semantics (SOS) is one of the most common formalisms for specifying language semantics. There has been much interest in automatically deriving small-step SOS definitions from big-step definitions and vice versa, as well as towards extrapolating language implementations from these inductive, declarative definitions. This work presents Computation-Tree Semantics (CTS) in which semantic configurations are tree-structured, unlike standard SOS-configurations which are "flat". This tree-structure is key in making our approach algorithmic, meaning it is able to describe how a transition is produced, contrary to the traditional declarative approach taken by SOS. We show how one can - in a straight-forward manner - obtain a CTS from the big-step semantics of a simple arithmetic language, a simple while language, and the call-by-need lambda-calculus as given by Launchbury. From the resulting CTS, we then obtain a small-step understanding of all these languages. The arithmetic language example is formalised in Coq/Rocq.
Many synthesizers implicitly benefit from using polymorphic types, since parametric polymorphism reduces the search space. Additional synthesis constraints may interfere with parametricity. In particular, a polymorphic type may cause otherwise feasible input-output examples to contradict each other. We present TAXI (type-and-example based inferencer), a tool for efficiently reasoning about the feasibility of polymorphic programs specified by input-output examples, and DRIVER, a tactic language for top-down program synthesis that uses feasibility reasoning to prune the search space. TAXI guarantees that every search state corresponds to a correct (albeit possibly partial) implementation. In addition, it allows for shortcutting the synthesis when a subspecification covers all cases. We show that these techniques have the potential to speed up top-down enumerative type-and-example driven synthesizers.
Syntactic sugars ease the definition of new language constructs by transforming them into an existing core language. Previous works lift independent typing rules and other semantics for these new constructs from the core language. The lifted semantics preserve the abstraction boundary of syntactic sugars, freeing users from inspecting desugared code that they did not write. While sugars may interact with contextual information during desugaring in general, these works are limited to simple sugars that do not. We identify a class of contextual sugars and present an extended algorithm for lifting their typing rules. With the addition of contexts, naively representing desugaring results in the core language may cause unexpected behavior and break hygiene. We introduce anchored terms that can point to the provenance of their contexts to represent desugaring results, which is similar to mechanisms used in Racket macros. Anchored terms need not concern authors or users of contextual sugars, but enable local reasoning. The lifted typing rules are sound with respect to the typing of anchored core language terms.
Choreographic programming provides a high-level abstraction for writing distributed computations while ensuring deadlock-freedom by construction. HasChor, a Haskell-based choreographic programming framework, offers a practical implementation of these ideas but faces limitations in handling an arbitrary number of participants and optimizing the communication of branches. In this work, we introduce CloudChor, a set of extensions that enhance HasChor's expressiveness and efficiency through the use of multiply-located values, allowing choreographies to distribute and collect data across multiple participants in a structured manner. Additionally, we refine HasChor's branching mechanism through a lightweight static analysis, selectively propagating branching decisions only to relevant participants, reducing communication overhead. To strengthen theoretical guarantees, we establish a formal semantics for HasChor and our extensions, proving deadlock-freedom. Finally, we demonstrate the practicality of our enhancements by implementing a data clean room protocol using CloudChor. Our contributions improve the applicability of choreographic programming to cloud-based secure data collaborations, making it a stronger candidate for real-world deployments.
An algebraic stepper is a pedagogical tool for showing the intermediate steps of program execution. This paper presents an algebraic stepper for OCaml that supports simple modules with hierarchical reference to variables (but without functors or signature sealing). When we program with modules, we can refer to a variable declared in a parent module directly, whereas we need to specify a module path to refer to a variable declared in a child module. Therefore, when we build the stepper, we attach a level to each variable (bound by let statement without in) and use it to maintain correct reference regardless of where a variable is used. In this paper, we present and formalize our stepper that implements delayed substitution of variables, and discuss the interplay between the stepper semantics and the level maintenance. We further show that the execution in the stepper semantics is consistent with the one in the standard small-step semantics. The resulting stepper is implemented, supporting most of the basic constructs of OCaml, and is used in an introductory OCaml course in the authors' institution.
The computing community has produced many high level languages and tools for programming high level systems (e.g. Java for user interfaces) and it has produced many low level languages and tools for programming low level systems (C for operating systems, Verilog for hardware design) yet there are not many examples of high level systems that have been produced to help develop low level systems. Sometimes this is due to a suspicion that the layers of abstraction that high level systems use incur unacceptable performance overheads. However, this talk attempts to challenge that view, giving examples of high level systems that improve the designer productivity for developing low level systems which also improve the quality of verification for low level systems. The talk will draw examples from the presenter’s own experience, as well as the work of others. Specific examples will include Lava and Bluespec for the design of hardware, the Silver Oak project for the co-design of a high assurance silicon root of trust, a Haskell-based DSL for programming machine learning chips, and recent work on the specification and verification of parts of a new silicon chip produced at Groq which makes use of the same Haskell DSL.
Editor calculi make it possible to describe the actions of syntax-directed editing and provide guarantees of safety through their specialized type system: Well-typed editor scripts produce well-formed programs. So far, such calculi have been language-specific. In this paper we present a generalized editor calculus, which can be used to specify a specialized syntax-directed editor for any language, given its abstract syntax. Moreover we show how to implement an editor generator that allows one to generate an editor calculus-based syntax-directed editor from a language specification. The generalized editor calculus can be encoded into a simply typed lambda calculus, extended with pairs, booleans, pattern matching and fixed points. This implies a general type safety result that holds for any instantiation.
The is-ought gap is a problem in moral philosophy observing that ethical judgments ("ought") cannot be grounded purely in truth judgments ("is"): that an ought cannot be derived from an is. This gap renders the following argument invalid: "It is true that type safe languages prevent bugs and that bugs cause harm, therefore you ought to write in type safe languages". To validate ethical claims, we must bridge the gap between is and ought with some ethical axiom, such as "I believe one ought not cause harm". But what do ethics have to do with manipulating programs? A lot! Ethics are central to correctness! For example, suppose an algorithm infers the type of is Bool, and is in fact a Bool; the program type checks. Is the program correct-does it behave as it ought? We cannot answer this without some ethical axioms: what does the programmer believe ought to be? I believe one ought to design and implement languages ethically. We must give the programmer the ability to express their ethics-their values and beliefs about a program-in addition to mere computational content, and build tools that respect the distinction between is and ought. This paper is a guide to ethical language design and implementation possibilities.
Meta-programming is the art of writing programs that produce or manipulate other programs. This allows programmers to automate error-prone or repetitive tasks, and exploit domain-specific knowledge to customize the generated code. Unfortunately, writing safe meta-programs remains very challenging, since errors in the generated code are usually only detected when running it, but not at the time when code is generated. How can we design a flexible and expressive meta-programming framework where we provide a range of safety guarantees about the code that is being generated and the code generator itself? We revisit Cocon, a type-theoretic framework for certified meta-programming. Cocon is a two-level type theory: at its base is the logical framework LF where we can represent domain-specific languages (DSL) ranging from simply-typed to polymorphic languages; on top sits a Martin-Loef type theory where we can write recursive programs and proofs about those DSLs using pattern matching. In particular, when the DSL is contained in Martin-Loef type theory we can use reflection and leverage MLTT's evaluation to execute programs written in a given DSL.Hence, we can derive type-safe meta-programming systems for a range of DSLs.
Foster et al. proposed a linguistic approach to the bidirectional transformation, with lens. A lens is a pair of two functions, one is a forward transformation called get which produces a target view from an original source, and the other is a backward transformation called put which updates the original source to a new one with an updated view. The get and put functions depend on each other to be consistent. A lens is called well-behaved if it satisfies two lens laws, GetPut and PutGet. Every put function uniquely determines a get function if it exists, as far as the get and put functions form a well-behaved lens. Fischer et al. found the conditions of a put function under which the corresponding get function exists, where both get and put functions are supposed to be total. In this paper, we consider the case where get and put functions are possibly partial. We show that almost the same conditions as the ones given by Fischer et al. work well when only a put function is possibly partial, while they do not work when a get function is also possibly partial. In order to have similar results, we propose a new lens law for the case where both get and put functions are possibly partial.
Programs are viewed as both functions to be executed and data structures to be analysed, but this has always required encoding, e.g. of a lambda-term to a syntax tree, so that a self-interpreter could not be applied to itself directly, but only to its code. Further, the code of a typed program should have a distinctive type. In a tree calculus, however, program analysis can be supported directly, without encodings, including the self-application of a breadth-first self-interpreter of type bf: for all X.for all Y.(X -> Y) -> (X -> Y).
This paper presents some ideas concerning program manipulation and program transformation from the early days of their development. Particular emphasis will be given to program transformation techniques in the area of functional programming and constraint logic programming. We will also indicate current applications of program transformation techniques to the verification of program properties and program synthesis.
Many programs which solve complicated problems can be seen as inversions of other, much simpler, programs. One particular example is transforming verifiers into solvers, which can be achieved with low effort by implementing the verifier in a relational language and then executing it in the backward direction. Unfortunately, as it is common with inverse computations, interpretation overhead may lead to subpar performance compared to direct program inversion. In this paper we discuss functional conversion aimed at improving relational miniKanren specifications with respect to a known fixed direction. Our preliminary evaluation demonstrates a significant performance increase for some programs which exemplify the approach.
Forty years ago development started on Mix, a partial evaluator designed specifically for the purpose of self-application. The effort, led by Neil D. Jones at the University of Copenhagen, eventually demonstrated that non-trivial compilers could be generated automatically by applying a partial evaluator to itself. The possibility, in theory, of such self-application had been known for more than a decade, but remained unrealized by the start of 1984. We describe the genesis of Mix, including the research environment, the challenges, and the main insights that led to success. We emphasize the critical role played by program annotation as a pre-processing step, later automated in the form of binding-time analysis.
A type-preserving compiler converts a well-typed input program into a well-typed output program. Previous studies have developed type-preserving compilers for various source languages, including the simply-typed lambda calculus and calculi with control constructs. Our goal is to realize type-preserving compilation of languages that have facilities for manipulating first-class continuations. In this paper, we focus on algebraic effects and handlers, a generalization of exceptions and their handlers with resumable continuations. Specifically, we choose an effect handler calculus and a typed stack-machine-based assembly language as the source and the target languages, respectively, and formalize the target language and a type preserving compiler. The main challenge posed by first-class continuation is how to ensure safety of continuation capture and resumption, which involves concatenation of unknown stacks. We solve this challenge by incorporating stack polymorphism, a technique that has been used for compilation from a language without first-class continuations to a stack-based assembly language. To prove that our compiler is type preserving, we implemented the compiler in Agda as a function between intrinsically typed ASTs. We believe that our contributions could lead to correct and efficient compilation of continuation-manipulating facilities in general.
A program generating a co-inductive data structure is called productive if the program eventually generates all the elements of the data structure. We propose a new method for verifying the productivity, which transforms a co-inductive data structure into a function that takes a path as an argument and returns the corresponding element. For example, an infinite binary tree is converted to a function that takes a sequence consisting of 0 (left) and 1 (right), and returns the element in the specified position, and a stream is converted into a function that takes a sequence of the form 0^n (or, simply a natural number n) and returns the n-th element of the stream. A stream-generating program is then productive just if the function terminates for every n. The transformation allows us to reduce the productivity verification problem to the termination problem for call-by-name higher-order functional programs without co-inductive data structures. We formalize the transformation and prove its correctness. We have implemented an automated productivity checker based on the proposed method, by extending an automated HFL(Z) validity checker, which can be used as a termination checker.
An attempt is made to record events leading up to the The 0'th PEPM Event: the October 1987 Partial Evaluation and Mixed Computation IFIP TC2 Working Conference at Gl. Avernæs, Denmark.
Neil Deaton Jones, professor emeritus at DIKU, the Department of Computer Science at the University of Copenhagen, passed away March 27th, 2023, shortly after his 82nd birthday. He is remembered for his seminal contributions to programming language research and theory of computation and for the impact his visions and his work have had on an entire generation of researchers, students and collaborators.
