By abstract machines I mean things like the SECD machine, Krivine's machine or more generally machines with states/memory/registers/stack/accumulator...

According to Wikipedia page of the Curry-Howard isomorphism, we have a correspondence with the Sequent Calculus where the left/right introductions rule matches with the constructors of codes and evaluation stacks. And the priority of rules application is related to call-by-value and call-by name reduction.

So I'm looking for more information than what we can find in Wikipedia.

  • 2
    $\begingroup$ Wikipedia lists a number of references. The Griffin, Parigot and Herbelin references are classic. I would recommend reading those first. $\endgroup$ – Andrej Bauer Mar 25 '17 at 20:57
  • 3
    $\begingroup$ Starting with A Functional Correspondence between Evaluators and Abstract Machines, there's been a string of work that directly connects abstract machines with evaluators. I've collected many (spiritual) successors here. Roughly speaking, given a Curry-Howard correspondence between a language and a logic, you can then use this approach to further get a correspondence to a particular abstract machine derived from an evaluator for the language. $\endgroup$ – Derek Elkins left SE Mar 26 '17 at 1:13

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.