52 citations · 106 across the 5 of their papers we have counts for
5 papers
Efficient Extensional Binary Tries
Andrew W Appel, Xavier Leroy
Lookup tables (finite maps) are a ubiquitous data structure. In pure functional languages they are best represented using trees instead of hash tables. In pure functional languages…
Proof Pearl: Magic Wand as Frame
Qinxiang Cao, Shengyi Wang, Aquinas Hobor +1
Separation logic adds two connectives to assertion languages: separating conjunction * ("star") and its adjoint, separating implication -* ("magic wand"). Comparatively, separating…
Verified Correctness and Security of mbedTLS HMAC-DRBG
Katherine Q. Ye, Matthew Green, Naphat Sanguansin +3
We have formalized the functional specification of HMAC-DRBG (NIST 800-90A), and we have proved its cryptographic security--that its output is pseudorandom--using a hybrid game-bas…
Separation Logic for Small-step Cminor
Andrew W. Appel, Sandrine Blazy
Cminor is a mid-level imperative programming language; there are proved-correct optimizing compilers from C to Cminor and from Cminor to machine language. We have redesigned Cminor…
Polymorphic lemmas and definitions in Lambda Prolog and Twelf
Andrew W. Appel, Amy P. Felty
Lambda Prolog is known to be well-suited for expressing and implementing logics and inference systems. We show that lemmas and definitions in such logics can be implemented with a…