OnDoc
| sign
in
up
~
pub
|
pdf
txt
html
toc
url
|
<<
>>
1
2
3
4
5
6
7
8
~
36
Table of Contents
1 Introduction
2 Memoization in Coq: state of the art
3 A primer on binary decision diagrams
4 Implementing BDDs in Coq.
5 Pure solutions
6 From pure data structures to persistent data structures via extraction
7 Discussion
8 Implementing reduction in the -calculus
9 Conclusion