Search Sciweavers | Sciweavers

22

ACL2
2006
ACM

262views Computational Linguistics» more ACL2 2006»

14 years 6 days ago

We introduce the logical story behind ﬁle input in ACL2 and discuss the types of theorems that can be proven about ﬁlereading operations. We develop a low level library for re...

Jared Davis

claim paper

Read More »

21

click to vote

ACL2
2006
ACM

247views Computational Linguistics» more ACL2 2006»

Parameterized congruences in ACL2

14 years 6 days ago

Download www.ccs.neu.edu

Support for congruence-based rewriting is built into ACL2. This capability allows ACL2 to treat certain predicate relations ”just like equality” under appropriate conditions a...

David Greve

claim paper

Read More »

21

click to vote

ACL2
2006
ACM

262views Computational Linguistics» more ACL2 2006»

Phylogenetic trees in ACL2

14 years 6 days ago

Download userweb.cs.utexas.edu

Biologists studying the evolutionary relationships between organisms use software packages to solve the computational problems they encounter. Several of these problems involve th...

Warren A. Hunt Jr., Serita M. Nelesen

claim paper

Read More »

14

click to vote

FMCAD
2006
Springer

113views Formal Methods» more FMCAD 2006»

An Integration of HOL and ACL2

13 years 10 months ago

Download www.cl.cam.ac.uk

We describe a link between the ACL2 and HOL mechanical proof assistants that enables the strengths of each system to be deployed smoothly within a single formal development. Severa...

Michael J. C. Gordon, James Reynolds, Warren A. Hu...

claim paper

Read More »

16

click to vote

ACL2
2006
ACM

258views Computational Linguistics» more ACL2 2006»

A robust machine code proof framework for highly secure applications

14 years 6 days ago