One of the main problems in Computer's Science is the problem of es-tablishing a rigorous bridge between programming languages and its correct implementation. In this work we establish a rigorous bridge between a the-oretical functional language (the ?l-calculus equipped with a deterministic reduction strategy, the weak head reduction) and an abstract implementation (the Krivine's abstract machine).
The work begins with the study of weak head reduction in ?l-calculus, starting with the standardization theorem proof, suggested by Loader. The relation between usual ?l-calculus and the de Bruijn (notation) ?l-calculus is formally established, as well as the relation between weak head reduction in both systems. It contains a complete proof that each term in the de Bruijn?l-calculus represents an a equivalence class in usual ?l-calculus. It is formally showed that lazy reduction in the calculus with explicit substitutions ?lr, of Curien, is a correct implementation of weak head reduction of closed terms in the de Bruijn ?l-calculus. It is also showed that Krivine's abstract machine correctly implements lazy reduction of closed closures in lr. Adding up the parts, the work shows that Krivine's machine correctly implements weak head reduction of closed terms in usual ?l-calculus.
The proof is rigorous, complete and explicit (contrasting, in a great measure, with related literature). It is also an incremental proof: the first step establishes the relation between the usual ?l-calculus and the de Bruijn? l-calculus (allowing to avoid a equivalence); the second step establishes the relation between the de Bruijn ?l calculus and the ?lr calculus (allowing to implement substitution explicitly); the third step establishes the relation between ?lr and the Krivine's machine (allowing the explicit search of the head expression in a sequence of applications).