C
An ACL2 library for C.
This library contains:
- A formalization of (a subset of) the C language.
This is a deep embedding of C in ACL2.
- A representation of (a subset of) the C language constructs in ACL2.
This is a shallow embedding of C in ACL2.
- A proof-generating C code generator for ACL2.
This recognizes, and translates to C,
the shallowly embedded ACL2 representation of C constructs,
and generates proofs based on the deep embedding.
The library is work in progress.
This library is based on the ISO/IEC 9899:2018 specification of C. In the documentation of this library,
this standard is referenced as `[C]';
sections are referenced
by appending their designations separated by colon,
e.g. `[C:6.2.6]' references Section 6.2.6;
paragraphs are referenced
by further appending their numbers separated by slash,
e.g. `[C:6.2.5/2]' references Paragraph 2 of Section 6.2.5.
These square-bracketed references may be used
as nouns or parenthetically.
Subtopics
- Atc
- ATC (ACL2 To C),
a proof-generating C code generator for ACL2.
- Language
- A formal model of (a subset of) the C language.
- Representation
- A representation of C in ACL2.
- Pack
- Build a symbol in the C package from a list of atoms.
