# 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