Name
Abstract | ||
|---|---|---|
ACL2, a Common Lisp-based language for programming and theorem proving, has enjoyed industrial success despite lacking modern language features such as a module system. In previous work, we equipped ACL2 with modules, interfaces, and explicit linking and measured our system with a series of experiments. One experiment revealed a serious lack of expressivity; the interfaces cannot describe the induction schemes necessary to reason about exported functions with nontrivial patterns of recursion. In this paper we revise our language, Modular ACL2, to overcome this weakness. The first novelty is the inclusion of manifest function definitions in interfaces from which ACL2 can infer induction schemes. The second novelty consists of the first proofs of soundness and expressivity for Modular ACL2; we also reaffirm the usefulness of our system with updated benchmarks. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1145/1599410.1599424 | PPDP |
Keywords | Field | DocType |
modular acl2,manifest function definition,modern language,common lisp-based language,induction scheme,serious lack,previous work,nontrivial pattern,industrial success,module system,theorem prover | Common Lisp,Programming language,Computer science,Automated theorem proving,Theoretical computer science,Mathematical proof,Modular design,Novelty,Soundness,ACL2,Recursion | Conference |
Citations | PageRank | References |
1 | 0.40 | 17 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Carl Eastlund | 1 | 38 | 2.68 |
| Matthias Felleisen | 2 | 3001 | 272.57 |