OnDoc
| sign
in
up
~
pub
|
pdf
txt
html
toc
url
|
<<
>>
1
~
29
30
31
32
33
34
35
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