1947-. French computer scientist, senior researcher at INRIA.
Proved the confluence theorem for abstract rewriting systems (1980), establishing that confluent reductions guarantee unique normal forms regardless of evaluation order.
Developed the Calculus of Constructions with Thierry Coquand, forming the theoretical basis for the Coq proof assistant.
Pioneered formal verification and type theory in functional programming.
His confluence results underpin interaction combinators and the HVM execution model: any reduction order reaches the same result, enabling massive parallelism.
Created computational linguistics tools for Sanskrit, bridging mathematical logic and natural language.