Resources for Students
This page lists resources for students interested in formal program verification and formal semantics of programming languages.
Formal Specification of Programming Languages
- Types and Programming Languages
Available at TUD’s library. Maybe the most popular introduction to formal programming language semantics. Topics include:- Operational small-step semantics
- Type systems
- Lamda calculus
- Software Foundations Series
Volumes 1 & 2 offer a solid introduction to the formal work on programming language semantics in Rocq (formerly known as Coq)- Volume 1: Logical Foundations introduces the interactive theorem prover Rocq
- Volume 2: Programming Language Foundations covers the fundamentals of formal PL specification:
- Operational small-step semantics
- Type systems
- Lambda calculus
- Hoare logic / pre & post conditions
Separation Logic
Separation logic is a powerful means to reason about imperative programs that work with the heap, e.g., C and Java programs. It is an extension of Hoare logic and hence follows the pre & post condition style reasoning.
- Wikipedia: Separation Logic
Very concise overview over the most important concepts. - Separation Logic and Concurrency (OPLSS 2016)
Very nice introduction to concurrent separation logic. Gives a good introduction from the ground up and also covers state-of-the art techniques/ extensions. Covers:- Basics: Heap cells, separation, frame rule
- Concurrency
- Fine-grained permissions
- Ghost state
- Recursive heap predicates to reason about data structures, e.g., lists, trees
- A Primer on Separation Logic
One of the first introductory works to separation logic. Not the easiest read. Covers:- Basics: Heap cells, separation, frame rule
- Recursive heap predicates to reason about data structures, e.g., lists, trees
- Software Foundations Vol. 6: Separation Logic Foundations
Gives a solid introduction to separation logic and its use in the interactive theorem prover Rocq (formerly known a Coq). (Like all SF books very Rocq focused.) Covers:- Basics: Heap cells, separation, frame rule
- Reasoning about data structures: Arrays, Lists
- SL flavours: Affine / intuitionistic SL vs linear / classical SL Focusses on classical / linear SL