Log in

No account? Create an account


Recent Entries




January 13th, 2019


The Symmetric Interaction Calculus is a minimal programming language and model of computation obtained by slightly modifying the Lambda Calculus so that it matches perfectly the abstract part of Lamping's optimal reduction algorithm. Characteristics:

Like the Lambda Calculus, it can easily express algebraic datatypes and arbitrary recursive algorithms.

Like Turing Machines, it can be evaluated through simple, constant-time operations.

Unlike the Lambda Calculus (and like Rust), it does not require garbage-collection.

Unlike the Lambda Calculus, all intermediate steps of its optimal reduction correspond to terms.

Unlike the Lambda Calculus, terms can be reduced not only optimally, but efficiently (i.e., no oracles).

Unlike both, it is intrinsically parallel.

It is isomorphic to symmetric interaction combinators, a beautiful model of computation.

December 31st, 2018


The call-by-push-value (CBPV) paradigm, inspired by monads, allows writing semantics for lambda-calculus without writing two variants to deal with the difference between call-by-name and call-by-value. To do so, CBPV introduces a term language that distinguishes computations and values, according to the slogan "a value is, a computation does"; this term language has a single evaluation order.


December 2nd, 2018


import scala.annotation.tailrec
import Thunk._

sealed trait Thunk[A, B] {
  @inline final def run(f: A => B): B = Thunk.run(this, f)
Read more...Collapse )

November 24th, 2018


Backtracking, Interleaving, and Terminating Monad Transformers

Oleg Kiselyov, Chung-chieh Shan, Daniel P. Friedman, Amr Sabry

We design and implement a library for adding backtracking com-
putations to any Haskell monad. Inspired by logic programming,
our library provides, in addition to the operations required by the
MonadPlus interface, constructs for fair disjunctions, fair conjunc-
tions, conditionals, pruning, and an expressive top-level interface.
Implementing these additional constructs is easy in models of
backtracking based on streams, but not known to be possible in
continuation-based models. We show that all these additional con-
structs can be generically and monadically realized using a single
primitive msplit. We present two implementations of the library:
one using success and failure continuations; and the other using
control operators for manipulating delimited continuations.

We describe the first implementation of multi-prompt delimited control op-
erators in OCaml that is direct in that it captures only the needed part of the
control stack. The implementation is a library that requires no changes to
the OCaml compiler or run-time, so it is perfectly compatible with existing
OCaml source and binary code.

November 23rd, 2018


This thesis addresses the interaction between recursive declarations and computational effects modeled by monads.
Zena M. Ariola, Aaron Bohannon, and Amr Sabry. Sequent calculi and abstract machines.


The reductions corresponding to the abstract machine transitions must occur at a bounded depth from the root of the syntax tree.

Although languages based on lambda-calculi have been successful in supporting reasoning about high-level programs, in this paper we focus on sequent calculi. We show that sequent calculi are more suitable for reasoning about abstract machines since they allow one to define an evaluator for terms in a tail-recursive fashion, thus satisfying the above criterion.


if the variable x stands for an unknown input in a command c, then the input abstraction μ̃x.c is a co-term that, when given a place to draw information, will bind that location to the input channel x while running c. Dually, if the co-variable α stands for an unknown output in a command c, then the output abstraction μα.c is a term that, when given a place to send information, will bind that location to the output channel α while running c.

November 19th, 2018


Atsushi Ohori

This paper presents a logical framework for low-level ma-
chine code and code generation. We first define a calculus, called
sequential sequent calculus, of intuitionistic propositional logic. A proof of the
calculus only contains left rules and has a linear (non-branching) struc-
ture, which reflects the properties of sequential machine code. We then
establish a Curry-Howard isomorphism between this proof system and
machine code based on the following observation. An ordinary machine
instruction corresponds to a polymorphic proof transformer that extends
a given proof with one inference step. A return instruction, which turns
a sequence of instructions into a program, corresponds to a logical ax-
iom (an initial proof tree). Sequential execution of code corresponds to
transforming a proof to a smaller one by successively eliminating the last
inference step. This logical correspondence enables us to present and an-
alyze various low-level implementation processes of a functional language
within the logical framework. For example, a code generation algorithm
for the lambda calculus is extracted from a proof of the equivalence the-
orem between the natural deduction and the sequential sequent calculus.
Powered by LiveJournal.com