Retour à la page du séminaire

###
27/01/99: Helmut Schwichtenberg (Munich) ---
Feasible programs from proofs.

**abstract**
We restrict induction and recursion on notations in all finite types so
as to characterize the polynomial time computable functions. The
restrictions are obtained by enriching the type structure with a
formation of types
and formulas
and
,
and by adding linear
concepts to the lambda-calculus (for object terms and proof terms). For
the arithmetical system we define modified realizability and show that
the programs extracted from proofs of -theorems characterize
the polynomial time computable functions.