diff --git a/index.md b/index.md index 5e2c031625b66786d38072e1716f2908815e1aaf..57aed0ec6cef5b4d93605027d85f3ac29105fa7b 100644 --- a/index.md +++ b/index.md @@ -5,4 +5,8 @@ menu: true menu_order: 1 --- -This research group focuses on mechanised language specification and program verification. We are exploring what it means to build, evaluate, and trust a fully mechanised language specification, using JavaScript as the real-world example language. We are developing library specifications which must be robust with respect to the environment: implementations should not leak; and specifications should be useful to the client. We are developing compositional program reasoning techniques that scale, leading to automatic tools for verifying properties of programs. Our current focus is on reasoning about JavaScript and Concurrency. Much of our work is based on Separation Logic. See details of our fourth-year/MSc course [here](https://psvg.doc.ic.ac.uk/teaching/separationlogic.html). +This research group focuses on mechanised language specification and program verification. +We are exploring what it means to build, evaluate, and trust a fully mechanised language specification, using JavaScript as the real-world example language. +We are developing library specifications which must be robust with respect to the environment: implementations should not leak; and specifications should be useful to the client. +We are developing compositional program reasoning techniques that scale, leading to automatic tools for verifying properties of programs. +Our current focus is on reasoning about JavaScript and Concurrency. Much of our work is based on Separation Logic. See details of our fourth-year/MSc course [here](/teaching/separationlogic.html). diff --git a/publications b/publications index 1b92f81b5d4a40cab2150c42035c98c5a5f152e3..6f5a6c5d0a76c933312e8bc279d7d61b6a31b881 160000 --- a/publications +++ b/publications @@ -1 +1 @@ -Subproject commit 1b92f81b5d4a40cab2150c42035c98c5a5f152e3 +Subproject commit 6f5a6c5d0a76c933312e8bc279d7d61b6a31b881 diff --git a/teaching/InferLab.md b/teaching/InferLab.md index f952cdd68f4aba5828e2e780b872d73d2e480a4f..2f04ddedb768ac3e9a429e8743ff2e0f98a44aa3 100644 --- a/teaching/InferLab.md +++ b/teaching/InferLab.md @@ -1,7 +1,7 @@ --- title: Separation Logic Infer Lab 2016 -project_id: infer -menu: true +project_id: infe +menu: false parent_menu: Teaching menu_order: 5 sub_menu_order: 2 diff --git a/teaching/ModelsComputation.md b/teaching/ModelsComputation.md index 731e991927d6ee7a416da6e566cd6b538614b1ef..39bf43f660ea4a8e67e1ed241483fdd7d0ee585e 100644 --- a/teaching/ModelsComputation.md +++ b/teaching/ModelsComputation.md @@ -1,7 +1,7 @@ --- title: Models of Computation project_id: moc -menu: true +menu: false parent_menu: Teaching menu_order: 5 sub_menu_order: 3 diff --git a/teaching/separationlogic.md b/teaching/separationlogic.md index 475b99774e32184f03d2e7e5172ab7dd5f592c07..8ebaafaadc0f5b93e6f4ce8dfbb72e0bd5a49ec0 100644 --- a/teaching/separationlogic.md +++ b/teaching/separationlogic.md @@ -1,7 +1,7 @@ --- title: Separation Logic project_id: sl -menu: true +menu: false parent_menu: Teaching menu_order: 5 sub_menu_order: 1