Lambda Mu Calculus and Duality: Call-by-Name and Call-by-Value

Jérôme Rocheteau

Under the extension of Curry-Howard's correspondence to classical logic, Gentzen's NK and LK systems can be seen as syntax-directed systems of simple types respectively for Parigot…