Writing Programs as QJ Proof and Compiling into Prolog Programs. - Yukihide Takayama (SLP, 1987)

QPC: QJ-based Proof Compiler - Simple Examples and Analysis. - Yukihide Takayama (ESOP, 1988)

Extended Projection - New Method to Extract Efficient Programs from Constructive Proofs. - Yukihide Takayama (FPCA, 1989)

Extraction of Redundancy-free Programs from Constructive Natural Deduction Proofs. - Yukihide Takayama (J. Symb. Comput., 1991)

QPC_2: A Constructive Calculus with Parameterized Specifications. - Yukihide Takayama (J. Symb. Comput., 1993)

Lifschitz' Logic of Calcubable Numbers and Optimizations in Program Extraction. - Susumu Hayashi; Yukihide Takayama (Logic, Language and Computation, 1994)

Defining Concurrent Processes Constructively. - Yukihide Takayama (Theor. Comput. Sci., 1994)

Extraction of Concurrent Processes from Higher Dimensional Automata. - Yukihide Takayama (CAAP, 1996)