## January 15th, 2019

## January 13th, 2019

https://medium.com/@maiavictor/the-abstract-calculus-fe8c46bcf39c

https://github.com/maiavictor/symmetric-interaction-calculus

https://pdfs.semanticscholar.org/1731/a6e49c6c2afda3e72256ba0afb34957377d3.pdf

https://pdfs.semanticscholar.org/6cfe/09aa6e5da6ce98077b7a048cb1badd78cc76.pdf

https://github.com/MaiaVictor/Formality

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.

https://github.com/maiavictor/symmetric-interaction-calculus

https://pdfs.semanticscholar.org/1731/a6e49c6c2afda3e72256ba0afb34957377d3.pdf

https://pdfs.semanticscholar.org/6cfe/09aa6e5da6ce98077b7a048cb1badd78cc76.pdf

https://github.com/MaiaVictor/Formality

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.

http://cs.ioc.ee/efftt/levy-slides.pdf

http://www.cs.bham.ac.uk/~pbl/papers/tlca99.pdf

http://www.cs.bham.ac.uk/~pbl/papers/thesisqmwphd.pdf

http://cs.ioc.ee/efftt/levy-slides.pdf

http://www.cs.bham.ac.uk/~pbl/papers/tlca99.pdf

http://www.cs.bham.ac.uk/~pbl/papers/thesisqmwphd.pdf

## 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

http://homes.sice.indiana.edu/ccshan/logicprog/LogicT-icfp2005.pdf

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.

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.

http://okmij.org/ftp/continuations/caml-shift-journal.pdf

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.

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

https://digitalcommons.ohsu.edu/cgi/viewcontent.cgi?article=1163&context=etd

This thesis addresses the interaction between recursive declarations and computational effects modeled by monads.

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.

https://www.cs.indiana.edu/~sabry/papers/sequent.pdf

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.

https://www.cs.indiana.edu/~sabry/papers/sequent.pdf

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

http://www.riec.tohoku.ac.jp/~ohori/research/flops99.pdf

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.

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.