Sciweavers

Top Ranked Papers of 2006 on Computational Linguistics | ACL2

All ConferencesACL2ACLCOLING Explore ACL2 2006 »

246

click to vote

ACL2
2006
ACM

296views Computational Linguistics» more ACL2 2006»

Combining ACL2 and an automated verification tool to verify a multiplier

15 years 7 months ago

Download www.ccs.neu.edu

We have extended the ACL2 theorem prover to automatically prove properties of VHDL circuits with IBM's Internal SixthSense verification system. We have used this extension to...

Erik Reeber, Jun Sawada

claim paper

Read More »

174

click to vote

ACL2
2006
ACM

283views Computational Linguistics» more ACL2 2006»

Towards a formal theory of on chip communications in the ACL2 logic

15 years 10 months ago

Download www.ccs.neu.edu

Julien Schmaltz, Dominique Borrione

claim paper

Read More »

185

click to vote

ACL2
2006
ACM

272views Computational Linguistics» more ACL2 2006»

Soundness of the simply typed lambda calculus in ACL2

15 years 10 months ago

Download userweb.cs.utexas.edu

To make it practical to mechanize proofs in programming language metatheory, several capabilities are required of the theorem proving framework. One must be able to represent and ...

Sol Swords, William R. Cook

claim paper

Read More »

149

click to vote

ACL2
2006
ACM

269views Computational Linguistics» more ACL2 2006»

ACL2 in DrScheme

15 years 10 months ago

Download www.ccs.neu.edu

Dale Vaillancourt, Rex L. Page, Matthias Felleisen

claim paper

Read More »

170

click to vote

ACL2
2006
ACM

267views Computational Linguistics» more ACL2 2006»

A verifying core for a cryptographic language compiler

15 years 10 months ago

Download www.cartesianclosed.com

A verifying compiler is one that emits both object code and a proof of correspondence between object and source code.1 We report the use of ACL2 in building a verifying compiler f...

Lee Pike, Mark Shields, John Matthews

claim paper

Read More »

Artificial Intelligence