Related papers: Row-Polymorphic Types for Strategic Rewriting
We describe several technical tools that prove to be efficient for investigating the rewrite systems associated with a family of algebraic laws, and might be useful for more general rewrite systems. These tools consist in introducing a…
We introduce a new two-sided type system for verifying the correctness and incorrectness of functional programs with atoms and pattern matching. A key idea in the work is that types should range over sets of normal forms, rather than sets…
As a contribution to the challenge of building game-playing AI systems, we develop and analyse a formal language for representing and reasoning about strategies. Our logical language builds on the existing general Game Description Language…
We present the design, implementation, and foundation of a verifier for higher-order functional programs with generics and recursive data types. Our system supports proving safety and termination using preconditions, postconditions and…
All formalizations of session types rely on linear types for soundness as session-typed communication channels must change their type at every operation. Embedded language implementations of session types follow suit. They either rely on…
Essentially, in a reversible programming language, for each forward computation from state $S$ to state $S'$, there exists a constructive method to go backwards from state $S'$ to state $S$. Besides its theoretical interest, reversible…
Coroutine, as a powerful programming construct, is widely used in asynchronous applications to replace thread-based programming or the callback hell. Using coroutines makes code more readable and maintainable, for its ability to transfer…
When trained on language data, do transformers learn some arbitrary computation that utilizes the full capacity of the architecture or do they learn a simpler, tree-like computation, hypothesized to underlie compositional meaning systems…
We propose a type system to analyze the time consumed by multi-threaded imperative programs with a shared global memory, which delineates a class of safe multi-threaded programs. We demonstrate that a safe multi-threaded program runs in…
We provide a compositional coalgebraic semantics for strategic games. In our framework, like in the semantics of functional programming languages, coalgebras represent the observable behaviour of systems derived from the behaviour of the…
Bringing the benefits of gradual typing to a language with parametric polymorphism like System F, while preserving relational parametricity, has proven extremely challenging: first attempts were formulated a decade ago, and several designs…
Many object-oriented dynamic languages allow programmers to _extract methods_ from objects and treat them as functions. This allows for flexible programming patterns, but presents challenges for type systems. In particular, a simple…
Curry-style system F, ie. system F with no explicit types in terms, can be seen as a core presentation of polymorphism from the point of view of programming languages. This paper gives a characterisation of type isomorphisms for this…
We give a polymorphic account of the relational algebra. We introduce a formalism of ``type formulas'' specifically tuned for relational algebra expressions, and present an algorithm that computes the ``principal'' type for a given…
Author stylized rewriting is the task of rewriting an input text in a particular author's style. Recent works in this area have leveraged Transformer-based language models in a denoising autoencoder setup to generate author stylized text…
Term rewriting plays a crucial role in software verification and compiler optimization. With dozens of highly parameterizable techniques developed to prove various system properties, automatic term rewriting tools work in an extensive…
Designers of autonomous agents, whether in physical or virtual environments, need to express nondeterminisim, failure, and parallelism in behaviors, as well as accounting for synchronous coordination between agents. Behavior Trees are a…
This paper proposes an adaptive neural-compilation framework to address the problem of efficient program learning. Traditional code optimisation strategies used in compilers are based on applying pre-specified set of transformations that…
Bidirectional typechecking, in which terms either synthesize a type or are checked against a known type, has become popular for its scalability (unlike Damas-Milner type inference, bidirectional typing remains decidable even for very…
Membrane systems are a biologically-inspired computational model based on the structure of biological cells and the way chemicals interact and traverse their membranes. Although their dynamics are described by rules, encoding membrane…