Name
Abstract | ||
|---|---|---|
Boyer and Moore's ACL2 theorem prover combines first-order applicative Common Lisp with a computational, first-order logic. While ACL2 has become popular and is being used for large programs, ACL2 forces programmers to rely on manually maintained protocols for managing modularity. In this paper, we present a prototype of Modular ACL2. The system extends ACL2 with a simple, but pragmatic functional module system. We provide an informal introduction, sketch a formal semantics, and report on our first experiences. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1007/978-3-540-92995-6_4 | PADL |
Keywords | Field | DocType |
pragmatic functional module system,first-order applicative,acl2 theorem prover,informal introduction,acl2 forces programmer,large program,modular acl2,practical module system,first-order logic,common lisp,formal semantics,theorem prover,first order,first order logic | Common Lisp,Programming language,Computer science,Automated theorem proving,Theoretical computer science,Modular design,Code reuse,ACL2,Functional module,Modularity,Sketch | Conference |
Volume | ISSN | Citations |
5418 | 0302-9743 | 2 |
PageRank | References | Authors |
0.39 | 12 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Carl Eastlund | 1 | 38 | 2.68 |
| Matthias Felleisen | 2 | 3001 | 272.57 |