Type-preserving compilation via dependently typed syntax (以英文演講)
- 講者Andreas Abel 教授 (哥德堡大学／查爾摩斯工學院)
邀請人：陳亮廷 - 時間2023-11-24 (Fri.) 14:00 ~ 15:00
- 地點資訊所舊館 108 演講廳
摘要
The *CompCert* project produced a verified compiler for a large fragment of the C programming language. The CompCert compiler is implemented in the type-theoretic proof assistant Coq, and is fully verified: there is a proof that the semantics of the source program matches the semantics of the target program. However, full verification comes with a price: the majority of the formalization is concerned not with the runnable code of the compiler, but with the properties of its components and proofs of these properties. If we are
*not* willing to pay the price of full verification, can we nevertheless profit from the technology of type-theoretic proof assistants to make our compilers *safer* and *less likely* to contain bugs?
In this talk, I am presenting a compiler for a small fragment of the C language using *dependently-typed syntax*.
A typical compiler is proceeding in phases: parsing, type checking, code generation, and finally, object/binary file creation. Parsing and type checking make up the *front end*, which may report syntax and type errors to the user; the other phases constitute the *back end* that should only fail in exceptional cases. After type checking succeeded, we have to deal only with well-typed source programs, whose abstract syntax trees can be captured with the indexed data types of dependently-typed proof assistants and programming languages like Agda, Coq, Idris, Lean etc.
More concisely, we shall by *dependently-typed syntax* refers to the technique of capturing well-typedness invariants of syntax trees.
Representing also typed assembly language via dependently-typed syntax, we can write a type-preserving compiler whose type soundness is given *by construction*. In the talk, the target of compilation is a fragment of the Java Virtual Machine (JVM) enriched by some *administrative
instructions* that declare the types of local variables. With JVM being a stack machine, instructions are indexed not only by the types of the local variables, but also by the types of the stack entries before and after the instruction. However for instructions that change the control flow, such as unconditional and conditional jumps, we need an additional structure to ensure type safety. Jumps are safe if the jump target has the same machine typing than the jump source. By *machine typing* we mean the pair of the types of the local variables and the types of the stack entries. Consequently, each label (i.e., jump target) needs to be assigned a machine type and can only be targeted from a program point with the same machine type. Technically, we represent labels as machine-typed de Bruijn indices, and control-flow instructions are indexed by a context of label types. We then distinguish two types of
labels:
Join points, e. g., labels of statements following an if-else
statement. Join points can be represented by a `let` binding in the
abstract JVM syntax.
Looping points, e. g., labels at the beginning of a while
statement that allow back jumps to iterate the loop. Those are
represented by `fix` (recursion).
Using dependently-typed machine syntax, we ensure that *well-typed jumps do not miss*. As a result, we obtain a type-preserving compiler by construction, with a good chance of full correctness, since many compiler faults already break typing invariants. Intrinsic well-typedness also allows us to write the compiler as a total function from well-typed source to typed assembly, and totality can be automatically verified by the Agda type and termination checker.
*not* willing to pay the price of full verification, can we nevertheless profit from the technology of type-theoretic proof assistants to make our compilers *safer* and *less likely* to contain bugs?
In this talk, I am presenting a compiler for a small fragment of the C language using *dependently-typed syntax*.
A typical compiler is proceeding in phases: parsing, type checking, code generation, and finally, object/binary file creation. Parsing and type checking make up the *front end*, which may report syntax and type errors to the user; the other phases constitute the *back end* that should only fail in exceptional cases. After type checking succeeded, we have to deal only with well-typed source programs, whose abstract syntax trees can be captured with the indexed data types of dependently-typed proof assistants and programming languages like Agda, Coq, Idris, Lean etc.
More concisely, we shall by *dependently-typed syntax* refers to the technique of capturing well-typedness invariants of syntax trees.
Representing also typed assembly language via dependently-typed syntax, we can write a type-preserving compiler whose type soundness is given *by construction*. In the talk, the target of compilation is a fragment of the Java Virtual Machine (JVM) enriched by some *administrative
instructions* that declare the types of local variables. With JVM being a stack machine, instructions are indexed not only by the types of the local variables, but also by the types of the stack entries before and after the instruction. However for instructions that change the control flow, such as unconditional and conditional jumps, we need an additional structure to ensure type safety. Jumps are safe if the jump target has the same machine typing than the jump source. By *machine typing* we mean the pair of the types of the local variables and the types of the stack entries. Consequently, each label (i.e., jump target) needs to be assigned a machine type and can only be targeted from a program point with the same machine type. Technically, we represent labels as machine-typed de Bruijn indices, and control-flow instructions are indexed by a context of label types. We then distinguish two types of
labels:
Join points, e. g., labels of statements following an if-else
statement. Join points can be represented by a `let` binding in the
abstract JVM syntax.
Looping points, e. g., labels at the beginning of a while
statement that allow back jumps to iterate the loop. Those are
represented by `fix` (recursion).
Using dependently-typed machine syntax, we ensure that *well-typed jumps do not miss*. As a result, we obtain a type-preserving compiler by construction, with a good chance of full correctness, since many compiler faults already break typing invariants. Intrinsic well-typedness also allows us to write the compiler as a total function from well-typed source to typed assembly, and totality can be automatically verified by the Agda type and termination checker.
BIO
Dr Abel is a Senior Lecturer at the Department of Computer Science and Engineering at Gothenburg University and Chalmers, Sweden and previously an Assistant Professor at Ludwig-Maximilians-University in Munich, Germany. He did his PhD at the University of Munich with Martin Hofmann on Type-Based Termination and habilitation and also at Munich on Normalization by Evaluation.
His research interests span programming languages, type systems, evaluation and compilation, termination, semantics, verification, proof languages, and logical foundations. He is the main developer of Agda and has contributed its entire components.
His research interests span programming languages, type systems, evaluation and compilation, termination, semantics, verification, proof languages, and logical foundations. He is the main developer of Agda and has contributed its entire components.