*By Robbert Krebbers, ICIS, Radboud University Nijmegen*

**This is an ongoing development. If you are looking for the Coq sources corresponding to specific papers, take a look here.**

The CH_{2}O project aims at formalizing novel features of the ISO C11 standard of the C programming language. CH_{2}O provides an operational, executable, and axiomatic semantics for a significant fragment of C11.

Our recent paper A Typed C11 Semantics for Interactive Theorem Proving at CPP 2015 gives a good overview of the CH_{2}O project.

- Robbert Krebbers. A Formal C11 Memory Model for Separation Logic. Draft.
- Robbert Krebbers and Freek Wiedijk. A Typed C11 Semantics for Interactive Theorem Proving. In CPP, pages 15-27, 2015.
- Robbert Krebbers. Separation algebras for C verification in Coq. In VSTTE, volume 8471 of LNCS, pages 150-166, 2014.
- Robbert Krebbers, Xavier Leroy and Freek Wiedijk. Formal C semantics: CompCert and the C standard. In ITP, volume 8558 of LNCS, pages 543-548, 2014.
- Robbert Krebbers. An operational and axiomatic semantics for non-determinism and sequence points in C. In POPL, pages 101-112, 2014.
- Robbert Krebbers. Aliasing restrictions of C11 formalized in Coq. In CPP, volume 8307 of LNCS, pages 50-65, 2013.
- Robbert Krebbers and Freek Wiedijk.
Separation Logic for Non-local Control Flow and Block Scope Variables.
In FoSSaCS, volume 7794 of LNCS, pages 257-272, 2013.

**Awarded best student contribution**. - Robbert Krebbers and Freek Wiedijk. A Formalization of the C99 Standard in HOL, Isabelle and Coq. In CICM, volume 6824 of LNAI, pages 297-299, 2011.

The most recent version of the Coq source code of this development can be downloaded here. Use:

scons -j [num cores]

to compile the development. This yields an executable called `ch2o`

that can be used to test the CH_{2}O semantics against actual C source files.

- base: interfaces, notations, and general theorems.
- tactics: general purpose tactics.
- proof_irrel: facts about proof irrelevant types/propositions.
- decidable: theorems on decidable structures.
- orders: theorems on ordered structures.
- option: the option monad, and various theorems on the option type.
- error: the error monad.
- list: miscellaneous definitions and theorems on lists.
- streams: miscellaneous definitions and theorems on streams.
- vector: miscellaneous definitions and theorems on vectors.
- numbers: miscellaneous facts on nat, N and Z.
- ars: theorems and definitions on abstract rewriting systems.
- collections: definitions, theorems, and tactics for collections.
- fin_collections: theorems on finite collections.
- listset: finite set implementation using unordered lists.
- fresh_numbers: generation of fresh numbers.
- prelude: exports all of the above.

- fin_maps: an interface and properties of finite maps.
- fin_map_dom: an interface and theorems for the domain function of finite maps.
- mapset: finite maps give rise to finite sets with extensional equality.
- natmap, pmap, nmap, zmap, and stringmap finite maps indexed by nat, positive, N, Z, and string.
- hashset: simple hashsets using finite maps over positive.

- integer_coding: abstract interface for integer representations.
- integer_operations: abstract interface for integer operations.
- type_classes: classes to overload notations for typing judgments.
- types: C types and type environments.
- type_environment: abstract interface for implementation defined properties.
- architecture_spec: type environment specifications based on concrete architectures.
- architectures: some specific architectures (ilp32, llp64 and lp64).

- separation: abstract interface and properties of separation algebras.
- separation_instances: boolean, fractional, counting, lockable and tagged separation algebras.
- permissions: the CH
_{2}O permission system as a separation algebra. - ctrees: separation algebra of abstract trees representing memory objects.
- cmap: separation algebra of abstract forests representing memories.

- memory_basics: basic definitions of the memory model.
- references: paths through types/ctrees.
- addresses (refinements): addresses into the memory.
- pointers (refinements): definition of pointers (address or NULL).
- pointer_bits (refinements): pointer fragment bits (pointer with index).
- bits (refinements): symbolic bits (0, 1, indeterminate, or pointer fragment).
- permission_bits (refinements and separation): bits annotated with permissions.
- memory_trees (refinements and separation): memory operations on C trees.
- memory_map (refinements and separation): memory operations on C maps.
- base_values (refinements): base values (void, indeterminate, integer, or pointer).
- values (refinements and separation): abstract values (base value, array, struct, or union).
- memory (refinements and separation): the CH
_{2}O memory model and its operations. - aliasing: abstract proof showing that type-based alias analysis is allowed.
- constant_propagation: abstract proof of constant propagation with respect to the memory model.

- assignments (separation): semantics of assignments.
- operations (refinements): semantics of casts, unary and binary operations.
- expressions: expressions and their decomposition into evaluation contexts.
- statements: statements and program contexts.
- state: the CH
_{2}O core C execution state. - smallstep: the CH
_{2}O core C small step operational semantics. - type_system (decidable): type judgments for expressions, statements, and states.
- type_preservation: type preservation and (weak) progress.

- memory_injections: functions to map a memory into another.
- refinement_classes: classes to overload notations for refinement judgments.
- refinements: basic definitions of the memory refinements.
- refinement_system: refinement judgments for expressions, statements, and states.
- refinement_preservation: preservation of refinements with respect to the operational semantics.

- expression_eval (correctness and separation): evaluation of constant expressions.
- executable: the CH
_{2}O core C executable semantics as a Coq function. - executable_sound and executable_complete: soundness and completeness of the executable semantics with respect to the operational semantics.
- frontend
(type soundness): CH
_{2}O abstract C and its type preserving translation into CH_{2}O core C. - interpreter (extraction): gluing the frontend and executable semantics together.

- memory_singleton: singleton memory.
- assertions: assertions of the separation logic.
- axiomatic_graph. Interpretation of the judgments of the separation logic.
- axiomatic. Interpretation of the judgments of the separation logic.
- axiomatic_expressions: inferences rules for expressions.
- axiomatic_functions: inferences rules for functions.
- axiomatic_statements: inference rules for statements.
- axiomatic_simple: inferences rules for expressions whose result is known.
- example_gcd: verification of Euclid's gcd algorithm.