update README and index page

README.md

@@ -72,7 +72,7 @@ make   # or make -j <number-of-cores-on-your-machine>
 - [VLSMs that Generate Logical Formulas](theories/Examples/Tutorial/Formulas.v): construction of VLSMs corresponding to propositional logic symbols, with their composition having well-formed propositional formulas as valid messages.
 - [VLSMs that Multiply](theories/Examples/Tutorial/Multiply.v): construction of VLSMs that perform arithmetic operations, with their composition having products of powers as valid messages.
 - [Primes Composition of VLSMs](theories/Examples/Tutorial/PrimesComposition.v): construction of an infinite family of VLSMs that multiply and their composition based on primes.
-- [Round-based Asynchronous Muddy Children Puzzle](theories/Examples/Tutorial/MuddyChildrenRounds.v): the [muddy children puzzle](https://plato.stanford.edu/entries/dynamic-epistemic/appendix-B-solutions.html#muddy) as a constrained composition of VLSMs that communicate asynchronously in rounds.
+- [Round-based Asynchronous Muddy Children Puzzle](theories/Examples/Tutorial/MuddyChildrenRounds.v): the [muddy children puzzle](https://plato.stanford.edu/entries/dynamic-epistemic/appendix-B-solutions.html#muddy) as a constrained composition of VLSMs that communicate asynchronously in rounds. For additional background, see the [first](https://www.youtube.com/watch?v=lTNG4HJ7V6U) and [second](https://www.youtube.com/watch?v=1H7kAW26pOA) part of a workshop presentation on the formalization.
 
 ### VLSM application: ELMO
 

meta.yml

@@ -127,7 +127,7 @@ documentation: |-
   - [VLSMs that Generate Logical Formulas](theories/Examples/Tutorial/Formulas.v): construction of VLSMs corresponding to propositional logic symbols, with their composition having well-formed propositional formulas as valid messages.
   - [VLSMs that Multiply](theories/Examples/Tutorial/Multiply.v): construction of VLSMs that perform arithmetic operations, with their composition having products of powers as valid messages.
   - [Primes Composition of VLSMs](theories/Examples/Tutorial/PrimesComposition.v): construction of an infinite family of VLSMs that multiply and their composition based on primes.
-  - [Round-based Asynchronous Muddy Children Puzzle](theories/Examples/Tutorial/MuddyChildrenRounds.v): the [muddy children puzzle](https://plato.stanford.edu/entries/dynamic-epistemic/appendix-B-solutions.html#muddy) as a constrained composition of VLSMs that communicate asynchronously in rounds.
+  - [Round-based Asynchronous Muddy Children Puzzle](theories/Examples/Tutorial/MuddyChildrenRounds.v): the [muddy children puzzle](https://plato.stanford.edu/entries/dynamic-epistemic/appendix-B-solutions.html#muddy) as a constrained composition of VLSMs that communicate asynchronously in rounds. For additional background, see the [first](https://www.youtube.com/watch?v=lTNG4HJ7V6U) and [second](https://www.youtube.com/watch?v=1H7kAW26pOA) part of a workshop presentation on the formalization.
 
   ### VLSM application: ELMO
 

resources/index.md

@@ -11,16 +11,22 @@ header-includes:
 ---
 
 <div style="text-align:left"><img src="https://github.githubassets.com/images/modules/logos_page/Octocat.png" height="25" style="border:0px">
-[View the project on GitHub](https://github.com/runtimeverification/casper-cbc-proofs)
+<a href="https://github.com/runtimeverification/vlsm">View the project on GitHub</a>
 <img src="https://github.githubassets.com/images/modules/logos_page/Octocat.png" height="25" style="border:0px"></div>
 
 ## About
 
 Welcome to the VLSM project website!
 
-A validating labelled state transition and message production system
-(VLSM) abstractly models a distributed system with faults. This project
-contains a formalization of VLSMs and their theory in the Coq proof assistant.
+The theory of Validating Labelled State transition and Message
+production systems (VLSMs) enables describing and proving properties
+of distributed systems executing in the presence of faults. This
+project contains a formalization of this theory in the Coq proof
+assistant along with several examples of distributed protocols
+modeled and verified using VLSMs, including the ELMO
+(Equivocation-Limited Message Observer) family of message
+validating protocols and the Paxos protocol for crash-tolerant
+distributed consensus.
 
 This is an open source project, licensed under the BSD 3-Clause "New" or "Revised" License.
 
@@ -31,7 +37,7 @@ The latest released version of VLSM can be [downloaded from GitHub](https://gith
 ## Documentation
 
 - [latest coqdoc presentation of the source files](latest/coqdoc/toc.html)
-- [latest Alectryon presentation the source files](latest/alectryon/toc.html)
+- [latest Alectryon presentation of the source files](latest/alectryon/toc.html)
 - [stdpp library](https://gitlab.mpi-sws.org/iris/stdpp)
 
 ## Help
@@ -48,7 +54,7 @@ Report [issues on GitHub](https://github.com/runtimeverification/vlsm/issues).
 - Karl Palmskog
 - Lucas Peña
 - Grigore Roșu
-- Traian Șerbănuță
+- Traian Florin Șerbănuță
 - Ioan Teodorescu
 - Dafina Trufaș
 - Jan Tušil