A Logical Approach to Compiler Construction Seminars/Workshops

Abstract

Parallel to the correspondence between the typed lambda calculus and the natural deduction proof system, it is possible to establish a correspondence between a low-level language (e.g. bytecode code and machine code) and a proof system of the intuitionistic propositional logic. This enables us to present compilation of the lambda calculus as a proof transformation from the natural deduction to a proof system of a low-level language.

In this talk, I will first analyze basic properties of compiler intermediate languages including A-normal forms, bytecode and machine code, and present proof systems corresponding to these languages. I will then show proof translation schemes from the natural deduction to those proof systems, and demonstrate the feasibility of the logical approach to compiling high-level languages. Finally, I will show that with further refinements of underlying proof systems, this paradigm can represent various compilation processes such as pattern matching compilation and register allocation in a clean and systematic way.