Related papers: Zero-Cost Coercions for Program and Proof Reuse
We classify programming languages according to evaluation order: each language fixes one evaluation order as the default, making it transparent to program in that evaluation order, and troublesome to program in the other. This paper…
There are two well-known formulations of recursive types: iso-recursive and equi-recursive types. Abadi and Fiore [1996] have shown that iso- and equi-recursive types have the same expressive power. However, their encoding of equi-recursive…
Herman et al. pointed out that the insertion of run-time checks into a gradually typed program could hamper tail-call optimization and, as a result, worsen the space complexity of the program. To address the problem, they proposed a…
We introduce constraints necessary for type checking a higher-order concurrent constraint language, and solve them with an incremental algorithm. Our constraint system extends rational unification by constraints x$\subseteq$ y saying that…
A circular program creates a data structure whose computation depends upon itself or refers to itself. The technique is used to implement the classic data structures circular and doubly-linked lists, threaded trees and queues, in a…
Type-level programming is an increasingly popular way to obtain additional type safety. Unfortunately, it remains a second-class citizen in the majority of industrially-used programming languages. We propose a new dependently-typed system…
In this paper, we provide a comprehensive, hands-on tutorial on how to apply deductive verification to programs written in OCaml. In particular, we show how one can use the GOSPEL specification language and the Cameleer tool to conduct…
We aim to reason about the correctness of behaviour-preserving transformations of Erlang programs. Behaviour preservation is characterised by semantic equivalence. Based upon our existing formal semantics for Core Erlang, we investigate…
We present a novel and well automatable approach to formal verification of programs with underspecified semantics, i.e., a language semantics that leaves open the order of certain evaluations. First, we reduce this problem to…
An inductive inference system for proving validity of formulas in the initial algebra $T_{\mathcal{E}}$ of an order-sorted equational theory $\mathcal{E}$ is presented. It has 20 inference rules, but only 9 of them require user interaction;…
Continuation Calculus (CC), introduced by Geron and Geuvers, is a simple foundational model for functional computation. It is closely related to lambda calculus and term rewriting, but it has no variable binding and no pattern matching. It…
We focus on control constructs that allow programmers define actions to be performed when respective conditions are met without requiring the explicit evaluation and testing of conditions as part of an imperative algorithm. Such elements…
In-context learning (ICL) has garnered significant attention for its ability to grasp functions/tasks from demonstrations. Recent studies suggest the presence of a latent task/function vector in LLMs during ICL. Merullo et al. (2024) showed…
Algorithm extraction aims to synthesize executable programs directly from models trained on algorithmic tasks, enabling de novo algorithm discovery without relying on human-written code. However, applying this paradigm to Transformer is…
This paper presents a novel approach to automatically verify properties of pure data-parallel programs with non-linear indexing -- expressed as pre- and post-conditions on functions. Programs consist of nests of second-order array…
This paper presents a method for inducing logic programs from examples that learns a new class of concepts called first-order decision lists, defined as ordered lists of clauses each ending in a cut. The method, called FOIDL, is based on…
In this paper we present a new static data type inference algorithm for logic programming. Without the need of declaring types for predicates, our algorithm is able to automatically assign types to predicates which, in most cases,…
Higher inductive types are inductive types that include nontrivial higher-dimensional structure, represented as identifications that are not reflexivity. While work proceeds on type theories with a computational interpretation of univalence…
Modern languages are equipped with static type checking/inference that helps programmers to keep a clean programming style and to reduce errors. However, the ever-growing size of programs and their continuous evolution require building fast…
Language models used in retrieval-augmented settings must arbitrate between parametric knowledge stored in their weights and contextual information in the prompt. This work presents a mechanistic study of that choice by extracting an…