the calculus of constructions applied to the derivation of correct programs, together with logic and automatic demonstration applied to system proof, circuit proof and program proof, the utilization of formal calculus proofs.
Proof environments:
the development, in particular, of Orme, an experimental platform for re-writing related software.
Fundamental aspects:
ordinals and recursive function hierarchies applied to termination, decision problems in real algebraic geometry and its application, termination of re-writing systems, the lambda-calculus, pi-calculus, and the theory of types, termination, equality handling, re-writing (divergence and schematizations, proof of equity of completion, higher-order re-writing), algebraic equations, program complexity, the generation of random structures, Luo software.
