Alba

Contents:

  • 1. Introduction
  • 2. Certified Programming
    • 2.1. Logic
    • 2.2. Natural Numbers
    • 2.3. Binary Natural Numbers
    • 2.4. List
    • 2.5. Vector
    • 2.6. Parsing
    • 2.7. Printf like Functions
  • 3. Language Elements
  • 4. Builtins
  • 5. Intermediate Representation
  • 6. Compilation
  • 7. Platforms
  • 8. Backends
  • 9. Draft
  • 10. Bibliography
Alba
  • 2. Certified Programming
  • View page source

2. Certified Programming

  • 2.1. Logic
    • 2.1.1. Function Composition
    • 2.1.2. Propositions
    • 2.1.3. Equality
    • 2.1.4. Decisions
    • 2.1.5. Refinement
  • 2.2. Natural Numbers
    • 2.2.1. Basic Definitions
    • 2.2.2. Zero is Different from a Successor
    • 2.2.3. Properties of Addition
    • 2.2.4. Properties of Multiplication
    • 2.2.5. Properties of Order
    • 2.2.6. Order and Predicates
    • 2.2.7. Difference
    • 2.2.8. Wellfounded Recursion
  • 2.3. Binary Natural Numbers
    • 2.3.1. Basic Definitions
  • 2.4. List
    • 2.4.1. Basics
    • 2.4.2. Append Lists
    • 2.4.3. List Reversal
  • 2.5. Vector
    • 2.5.1. Basics
    • 2.5.2. Concatenate Vectors
    • 2.5.3. Reverse Vectors
    • 2.5.4. Random Access
  • 2.6. Parsing
    • 2.6.1. String Parser
    • 2.6.2. Incremental Parsers
    • 2.6.3. Backtracking (DRAFT)
  • 2.7. Printf like Functions
Previous Next

© Copyright 2021, Helmut Brandl.

Built with Sphinx using a theme provided by Read the Docs.