Notes on the computational content of classical logic

• About Urban's notations, Lengrand's λξ and van Bakel et al' X (2011)
  We compare Urban's term notation and semantics for LK with Lengrand's λξ-calculus and with van Bakel et al's X calculus.
  
  
• About Danos-Joinet-Schellinx's LK^tq (2010)
  We give a (partial) reformulation of Danos-Joinet-Schellinx “A new deconstructive logic: linear logic” (DJS) from a computational point of view, by reexpressing the main definitions of the paper using a variant of the μμ̃-system as language of proofs.
  
  
• About Rehof-Sørensen's λδ and Felleisen's F (in French, 2007)
  We show Rehof-Sørensen's λδ-calculus is built on Felleisen's F control operator, and thus cannot support a satisfactory call-by-name reduction semantics.
  
  
• About Felleisen's C operator (2004)
  We address the mismatch between typing Felleisen's C operator of type ¬¬A → A and the need for a non-⊥ toplevel. We compare the approaches of Griffin, Krivine and Ariola-Herbelin in solving this issue. We propose a more relevant typing for C than ¬¬A → A (see also the conclusion of the JFP07 paper).

Notes on λ-bar-μμ̃ and abstract machines

• Biernacki et al's S-machine in λ-bar-μμ̃ (2005)
  This is an example to advocate the well-suitedness of λ-bar to express various abstract machines.

Notes on CPS-translations

• A memo on the different CPS for delimited control (with comments in French, 2011)
  We compare Danvy-Filinski's double CPS, Plotkin's simple CPS, Kameyama-Hasegawa's double CPS.