Data Types, Infinity and Equality in System AF2. - Christophe Raffalli (CSL, 1993)

A Semantical Storage Operator Theorem for All Types. - Christophe Raffalli (Ann. Pure Appl. Log., 1998)

Completeness, minimal logic and programs extraction. - Christophe Raffalli (Theor. Comput. Sci., 2001)

System ST beta-reduction and completeness. - Christophe Raffalli (LICS, 2003)

System ST toward a type system for extraction and proofs of programs. - Christophe Raffalli (Ann. Pure Appl. Log., 2003)

Simple proof of the completeness theorem for second-order classical and intuitionistic logic by reduction to first-order mono-sorted logic. - Karim Nour; Christophe Raffalli (Theor. Comput. Sci., 2003)

An experiment concerning mathematical proofs on computers with French undergraduate students. - René David; Christophe Raffalli (J. Appl. Log., 2004)

Getting results from programs extracted from classical proofs. - Christophe Raffalli (Theor. Comput. Sci., 2004)

PhoX. - Christophe Raffalli; Paul Rozière (The Seventeen Provers of the World, 2006)

Realizability of the Axiom of Choice in HOL. (An Analysis of Krivine's Work). - Christophe Raffalli; Frédéric Ruyer (Fundam. Informaticae, 2008)

Some properties of random lambda terms - René David; Christophe Raffalli; Guillaume Theyssier; Katarzyna Grygiel; Jakub Kozik; Marek Zaionc (Log. Methods Comput. Sci., 2009)

MathAbs: a representational language for mathematics. - Muhammad Humayoun; Christophe Raffalli (FIT, 2010)

Subtyping-Based Type-Checking for System F with Induction and Coinduction. - Rodolphe Lepigre; Christophe Raffalli (CoRR, 2016)

Abstract Representation of Binders in OCaml using the Bindlib Library. - Rodolphe Lepigre; Christophe Raffalli (LFMTP@FSCD, 2018)

Practical Subtyping for Curry-Style Languages. - Rodolphe Lepigre; Christophe Raffalli (ACM Trans. Program. Lang. Syst., 2019)