Name
Abstract | ||
|---|---|---|
Dependently typed languages have for a long time been used to describe proofs about programs. Traditionally, dependent types are used mostly for stating and proving the properties of the programs and not in defining the programs themselves. An impressive ex- ample is the certified compiler by Leroy (2006) implemented and proved correct in Coq (Bertot and Cast´ eran 2004). |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1145/1481861.1481862 | Advanced Functional Programming |
Keywords | DocType | Citations |
dependent types,programming references | Conference | 4 |
PageRank | References | Authors |
0.81 | 2 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ulf Norell | 1 | 133 | 9.21 |
| Yves Bertot | 2 | 442 | 40.82 |