Wolfgang Schreiner

Thinking Programs

Logical Modeling and Reasoning about Languages, Data, Computations, and Executions

Second Edition [First Edition]

© 2025 Springer Texts & Monographs in Symbolic Computation

SpringerLink Page
Buy hardcover or eBook version (free PDF access from JKU campus network)

Errata
Errors in the published version of the book.

• Exercises
  1. Syntax and Semantics
  2. The Language of Logic
  3. The Art of Reasoning
  4. Building Models
  5. Recursion
  6. Abstract Data Types
  7. Programming Languages
  8. Computer Programs
  9. Concurrent Systems
• Software Examples
  1. Abstract Syntax Trees with OCaml
  2. The Logic of the RISC ProofNavigator
  3. Reasoning with the RISC ProofNavigator
  4. Writing Definitions in Isabelle/HOL
  5. Recursive Definitions in Isabelle/HOL
  6. Abstract Data Types in CafeOBJ
  7. Abstract Data Types in CASL
  8. Denotational Semantics in OCaml
  9. Operational Semantics in the K Framework
  10. Operational Semantics in the K Framework (Test Program)
  11. Program Reasoning in RISCAL
  12. Program Resoning in the RISC ProgramExplorer
  13. System Analysis in TLA+
  14. System Analysis in RISCAL
• Software Systems
  • OCaml
  • SLANG
  • RISC ProofNavigator
  • Isabelle/HOL
  • CafeOBJ
  • CASL/Hets
  • K Framework
  • RISCAL
  • RISC ProgramExplorer
  • TLA⁺

---

Wolfgang Schreiner

Last modified: March 13, 2026