diff --git a/ConcurrentSeparationLogic.v b/ConcurrentSeparationLogic.v index 05f83ba..6415b91 100644 --- a/ConcurrentSeparationLogic.v +++ b/ConcurrentSeparationLogic.v @@ -1,5 +1,5 @@ (** Formal Reasoning About Programs - * Chapter 19: Concurrent Separation Logic + * Chapter 20: Concurrent Separation Logic * Author: Adam Chlipala * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *) diff --git a/Connecting.v b/Connecting.v index 8624407..c25fdee 100644 --- a/Connecting.v +++ b/Connecting.v @@ -1,5 +1,5 @@ (** Formal Reasoning About Programs - * Chapter 16: Connecting to Real-World Programming Languages and Platforms + * Chapter 17: Connecting to Real-World Programming Languages and Platforms * Author: Adam Chlipala * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *) diff --git a/DeepAndShallowEmbeddings.v b/DeepAndShallowEmbeddings.v index 57e98d2..ec1b18d 100644 --- a/DeepAndShallowEmbeddings.v +++ b/DeepAndShallowEmbeddings.v @@ -1,5 +1,5 @@ (** Formal Reasoning About Programs - * Chapter 14: Deep and Shallow Embeddings + * Chapter 15: Deep and Shallow Embeddings * Author: Adam Chlipala * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *) diff --git a/HoareLogic.v b/HoareLogic.v index a73f190..1ca0273 100644 --- a/HoareLogic.v +++ b/HoareLogic.v @@ -1,5 +1,5 @@ (** Formal Reasoning About Programs - * Chapter 13: Hoare Logic: Verifying Imperative Programs + * Chapter 14: Hoare Logic: Verifying Imperative Programs * Author: Adam Chlipala * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *) diff --git a/MessagesAndRefinement.v b/MessagesAndRefinement.v index 5756fbb..0e3238a 100644 --- a/MessagesAndRefinement.v +++ b/MessagesAndRefinement.v @@ -1,5 +1,5 @@ (** Formal Reasoning About Programs - * Chapter 20: Process Algebra and Behavioral Refinement + * Chapter 21: Process Algebra and Behavioral Refinement * Author: Adam Chlipala * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *) diff --git a/ProgramDerivation.v b/ProgramDerivation.v index bb0d3c1..0575b30 100644 --- a/ProgramDerivation.v +++ b/ProgramDerivation.v @@ -1,5 +1,5 @@ (** Formal Reasoning About Programs - * Chapter 17: Deriving Programs from Specifications + * Chapter 18: Deriving Programs from Specifications * Author: Adam Chlipala * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ * Some material borrowed from Fiat *) diff --git a/SeparationLogic.v b/SeparationLogic.v index 492ac35..7368414 100644 --- a/SeparationLogic.v +++ b/SeparationLogic.v @@ -1,5 +1,5 @@ (** Formal Reasoning About Programs - * Chapter 15: Separation Logic + * Chapter 16: Separation Logic * Author: Adam Chlipala * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *) diff --git a/SessionTypes.v b/SessionTypes.v index f11a70a..c62cea0 100644 --- a/SessionTypes.v +++ b/SessionTypes.v @@ -1,5 +1,5 @@ (** Formal Reasoning About Programs - * Chapter 21: Session Types + * Chapter 22: Session Types * Author: Adam Chlipala * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *) diff --git a/SharedMemory.v b/SharedMemory.v index 68f3df4..822d809 100644 --- a/SharedMemory.v +++ b/SharedMemory.v @@ -1,5 +1,5 @@ (** Formal Reasoning About Programs - * Chapter 18: Operational Semantics for Shared-Memory Concurrency + * Chapter 19: Operational Semantics for Shared-Memory Concurrency * Author: Adam Chlipala * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *) diff --git a/TypesAndMutation.v b/TypesAndMutation.v index 5da5627..e563fa3 100644 --- a/TypesAndMutation.v +++ b/TypesAndMutation.v @@ -1,5 +1,5 @@ (** Formal Reasoning About Programs - * Chapter 12: Types and Mutation + * Chapter 13: Types and Mutation * Author: Adam Chlipala * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *)