ICFP

The class of Infinitary inductive-recursive (InfIR) types is commonly used to model type theory within itself. While it is common and convenient to provide examples of values within an InfIR model, writing functions that manipulate InfIR types is an ...

A lot of the expressive power of array-oriented languages such as Iverson's APL and J comes from their implicit lifting of scalar operations to act on higher-ranked data, for example to add a value to each element of a vector, or to add two compatible ...

Algebraic effects and effect handlers provide a modular abstraction for effectful programming. They support user-defined effects, as in Haskell, in conjunction with direct-style effectful programming, as in ML. They also present a structured interface ...

We introduce a library called CSP-Agda for representing processes in the dependently typed theorem prover and interactive programming language Agda. We will enhance processes by a monad structure. The monad structure facilitates combining processes in a ...

We describe a generic approach to defining partially-static data and corresponding operations.

Parameterized monad goes beyond monads in letting us represent type-state. An effect executed by a computation may change the set of effects it may be allowed to do afterwards. We describe how to easily `add' and `subtract' such type-state effects. ...

In this paper, we develop a library of typed proof search procedures, and demonstrate their remarkable utility as a mechanism for proof-search and automation. We describe a framework for describing proof-search procedures in Agda, with a library of ...

Type-directed programming is a powerful programming paradigm where rich types dictate the structure of the program, making design largely automatic. While mechanical, this paradigm still requires manual reasoning that is both tedious and error-prone. ...

We discuss a generalization of the synchronization mechanism selective choice. We argue that selective choice can be extended to synchronize arbitrary data structures of events, based on a typing paradigm introduced by McBride: the derivatives of ...

We define a block based matrix representation in Agda and lift various algebraic structures (semi-near-rings, semi-rings and closed semi-rings) to matrices in order to verify algorithms that can be implemented using the closure operation in a semi-...

Many version control systems, including Git and Mercurial, rely on <pre>diff3</pre> to merge different revisions of the same file. More precisely <pre>diff3</pre> automatically merges two text files, given a common base version, comparing them line by ...