|
|
|
|
|
|
Foreword |
1 | Raja Natarajan |
|
|
Proof assistants: History, ideas and future |
3 |
H Geuvers |
|
|
Operating system verification—An overview |
27 |
Gerwin Klein |
|
|
A compact kernel for the calculus of inductive constructions |
71 | A Asperti, W Ricciotti, C Sacerdoti Coen and E Tassi | Click |
|
Proving the correctness of client/server software |
145 | Eyad Alkassar, Sebastian Bogan and Wolfgang J Paul |
|
|
Formalizing Arrow’s theorem |
193 |
Freek Wiedijk |
|