Paul Brauner, Clément Houtmann & Claude Kirchner (2007):
Principles of Superdeduction.
In: LICS,
pp. 41–50.
Serenella Cerrito & Delia Kesner (2004):
Pattern matching as cut elimination.
Theor. Comput. Sci. 323(1-3),
pp. 71–127.
Horatiu Cirstea & Claude Kirchner (2001):
The rewriting calculus –- Part I and II.
Logic Journal of the Interest Group in Pure and Applied Logics 9(3),
pp. 427–498.
Pierre-Louis Curien & Hugo Herbelin (2000):
The duality of computation.
In: ICFP,
pp. 233–243.
Pierre-Louis Curien & Guillaume Munch-Maccagnoni (2010):
The duality of computation under focus.
In: IFIP TCS.
Accepted.
Gilles Dowek, Thérèse Hardin & Claude Kirchner (2003):
Theorem Proving Modulo.
Journal of Automated Reasoning 31(1),
pp. 33–72.
Clément Houtmann (2008):
Axiom Directed Focusing.
In: TYPES,
pp. 169–185.
Clément Houtmann (2010):
Représentation et interaction des preuves en superdéduction modulo.
Ph.D. thesis.
Université Henri Poincaré, Nancy Universit\IeC és.
Chuck Liang & Dale Miller (2007):
Focusing and Polarization in Intuitionistic Logic.
In: CSL,
pp. 451–465.
Chuck Liang & Dale Miller (2009):
A Unified Sequent Calculus for Focused Proofs.
In: LICS.
IEEE Computer Society,
pp. 355–364.
Guillaume Munch-Maccagnoni (2009):
Focalisation and Classical Realisability.
In: CSL,
pp. 409–423.
Emmanuel Polonowski (2004):
Strong Normalization of lambda-mu-mu/tilde-Calculus with Explicit Substitutions.
In: FoSSaCS,
pp. 423–437.
Christian Urban (2000):
Classical Logic and Computation.
Ph.D. thesis.
University of Cambridge.
Benjamin Wack (2005):
Typage et déduction dans le calcul de réécriture.
Ph.D. thesis.
Université Henri Poincaré, Nancy 1.
Noam Zeilberger (2008):
Focusing and higher-order abstract syntax.
In: POPL,
pp. 359–369.