![](https://dblp.uni-trier.de./img/logo.320x120.png)
![search dblp search dblp](https://dblp.uni-trier.de./img/search.dark.16x16.png)
![search dblp](https://dblp.uni-trier.de./img/search.dark.16x16.png)
default search action
Archive of Formal Proofs, Volume 2008
Volume 2008, 2008
- Tobias Nipkow:
Quantifier Elimination for Linear Arithmetic. - Klaus Aehlig, Tobias Nipkow:
Normalization by Evaluation. - Norbert Schirmer:
A Sequential Imperative Programming Language Syntax, Semantics, Hoare Logics and Verification Environment. - Veronika Ortner, Norbert Schirmer:
BDD Normalisation. - Michael Nedzelsky:
Recursion Theory I. - Filip Maric:
Formal Verification of Modern SAT Solvers. - Tobias Nipkow:
Fun With Functions. - Tobias Nipkow:
Arrow and Gibbard-Satterthwaite. - Gregor Snelting, Daniel Wasserrab:
A Correctness Proof for the Volpano/Smith Security Typing System. - Daniel Wasserrab:
Towards Certified Slicing. - Jasmin Christian Blanchette:
The Textbook Proof of Huffman's Algorithm. - Tobias Nipkow, Lawrence C. Paulson:
Fun With Tilings. - Peter Gammie:
Some classical results in Social Choice Theory. - Lennart Beringer, Martin Hofmann:
Secure information flow and program logics. - Lennart Beringer, Martin Hofmann:
A Bytecode Logic for JML and Types.
![](https://dblp.uni-trier.de./img/cog.dark.24x24.png)
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.