Core C++

 Core C++🔗

Compiled2026-10-01T20:19:55ZProject332d8b5Revert "The std::function with no target is null, as nullptr gives it in C++"Leanleanprover/lean4:v4.32.2VersoBlueprintv4.32.0@84fafd488acf

Core C++ is a subset of C++17 with an LL(1) grammar, a deterministic semantics and no undefined behaviour.

This blueprint holds the lexer, the grammar, and the typing and evaluation rules in natural semantics, in the sequent style of Kahn (1987), and points each rule to the Lean code that implements it in core-cpp/CoreCpp/.

The source, the interpreter and this blueprint live in the repository github.com/ChristianoBraga/corecpp.

One chapter per group of constructions, one node per construction or nonterminal. The design lists no construction the blueprint leaves out.

Contents

  1. 1. Lexer and grammar
  2. 2. Judgments and domains
  3. 3. Types and expressions
  4. 4. Storage and commands
  5. 5. Abstraction
  6. 6. Encapsulation
  7. 7. Type systems
  8. 8. The standard library
  9. 9. References
  10. Dependency Graph
  11. Blueprint Summary