diff --git a/_includes/head.html b/_includes/head.html
index 24aabf795e5026a9fb25f9f4f7de7365769782d4..7f53b7d3b194e7f0b51e038479937b569737bb4a 100644
--- a/_includes/head.html
+++ b/_includes/head.html
@@ -22,6 +22,5 @@
ga('create', 'UA-47856851-3', 'auto');
ga('send', 'pageview');
-
</script>
</head>
diff --git a/_includes/header.html b/_includes/header.html
index b1326e7f1ebd6d0e1d0015f47aa485e763590af4..448d7b34e55b66b4a13f4d18a65bec6348e8dfa9 100644
--- a/_includes/header.html
+++ b/_includes/header.html
@@ -2,15 +2,46 @@
<div class="site-masthead">
<div class="container">
<nav class="nav">
- {% assign menu_items = site.pages | where:"menu",true | sort:"menu_order" %}
- {% if menu_items.size > 1 %}
- {% for item in menu_items %}
- {% if item.title %}
- <a class="nav-link {% if item.url == page.url %}active{% endif %}" href="{{ item.url | prepend: site.baseurl
- }}">{{ item.title }}</a>
- {% endif %}
+
+ {% for menu_index in (1..10) %}
+ {% assign menu_items = site.pages | where:"menu",true | where: "menu_order",menu_index %}
+ {% if menu_items.size > 0 %}
+ {% if menu_items.first.parent_menu %}
+ {% assign check_url = menu_items.first.parent_menu | downcase | prepend: '/' | append: '/' %}
+ <li class="dropdown">
+ <a class="nav-link {% if page.url contains check_url %}active{% endif %} dropbtn" href="#">{{ menu_items.first.parent_menu }}</a>
+ <div class="dropdown-content">
+ {% for item in menu_items %}
+ <a class="nav-link {% if item.url == page.url %}active{% endif %}" href="{{ item.url | prepend: site.baseurl }}">{{ item.title }}</a>
+ {% endfor %}
+ </div>
+ </li>
+ {% else %}
+ {% for item in menu_items %}
+ <li><a class="nav-link {% if item.url == page.url %}active{% endif %}" href="{{ item.url | prepend: site.baseurl }}">{{ item.title }}</a></li>
+ {% endfor %}
+ {% endif %}
+ {% endif %}
{% endfor %}
- {% endif %}
+ <!--{% assign menu_items = site.pages | where:"menu",true | sort:"menu_order" %}-->
+ <!--{% if menu_items.size > 1 %}-->
+ <!--{% for item in menu_items %}-->
+ <!--{% if item.title %}-->
+ <!--{% if item.parent_menu %}-->
+ <!--<li class="dropdown">-->
+ <!--<a class="nav-link dropbtn" href="#">{{ item.parent_menu }}</a>-->
+ <!--{% assign sub_menu_items = site.pages | where:"menu",true | sort:"menu_order" %}-->
+ <!--<div class="dropdown-content">-->
+ <!--<a class="nav-link" href="#">aaaaaaaa</a>-->
+ <!--<a class="nav-link" href="#">bbbbbbbb</a>-->
+ <!--</div>-->
+ <!--</li>-->
+ <!--{% else %}-->
+ <!--<li><a class="nav-link {% if item.url contains page.url %}active{% endif %}" href="{{ item.url | prepend: site.baseurl }}">{{ item.title }}</a></li>-->
+ <!--{% endif %}-->
+ <!--{% endif %}-->
+ <!--{% endfor %}-->
+ <!--{% endif %}-->
</nav>
</div>
</div>
diff --git a/_layouts/home.html b/_layouts/home.html
index cb7083c882243fadbfff3e8f2d5a0dd2a2c0e2ba..ff29dae31c4b4345109d09935b087c7a9cc04d5e 100644
--- a/_layouts/home.html
+++ b/_layouts/home.html
@@ -7,10 +7,7 @@ layout: default
</div>
{% assign research_pages = site.pages | where_exp: 'page', 'page.url contains "/research/"'%}
{% for item in research_pages reversed %}
- {% if item.url contains "separationlogic" %}
- {% else %}
<a class="btn btn-primary btn-lg" href="{{ item.url }}">{{ item.title }}</a>
- {% endif %}
{% endfor %}
</div>
diff --git a/assets/blog.scss b/assets/blog.scss
index 43303fe71383ae9cb5e78a9b6e099dd90ea65c77..27c4a43ab9c063697edfa8fd77577910284164c0 100644
--- a/assets/blog.scss
+++ b/assets/blog.scss
@@ -72,6 +72,24 @@ h6, .h6 {
*/
.site-masthead {
+ li{
+ display:inline-block;
+ }
+
+ .dropdown-content {
+ display: none;
+ position: absolute;
+ background-color: $primary_colour;
+ min-width: 160px;
+ background-color: $primary_colour;
+ -webkit-box-shadow: inset 0 -.1rem .25rem rgba(0,0,0,.2);
+ box-shadow: inset 0 -.1rem .25rem rgba(0,0,0,.2);
+ }
+
+ .dropdown:hover .dropdown-content {
+ display: block;
+ }
+
margin-bottom: 3rem;
background-color: $primary_colour;
-webkit-box-shadow: inset 0 -.1rem .25rem rgba(0,0,0,.2);
diff --git a/research/concurrency.md b/research/concurrency.md
index f218902e568cb8c2a4f99b500b1e49e799461adb..9a07d43528679e6a7767456f4e9b2524ce768ecb 100644
--- a/research/concurrency.md
+++ b/research/concurrency.md
@@ -2,7 +2,9 @@
title: Concurrency
project_id: concurrency
menu: true
+parent_menu: Research
menu_order: 3
+sub_menu_order: 1
---
We develop formal reasoning techniques for concurrent programs, with a
diff --git a/research/javascript.md b/research/javascript.md
index 2d9ab8c93b7e9f40632c5cd7857d364736173e27..7f2887a50e55cd08eae75fd88ec959efcdccb7be 100644
--- a/research/javascript.md
+++ b/research/javascript.md
@@ -2,7 +2,9 @@
title: JavaScript
project_id: web
menu: true
-menu_order: 4
+parent_menu: Research
+menu_order: 3
+sub_menu_order: 2
---
We study the mechanised specification of the JavaScript language
diff --git a/research/separationlogic.md b/teaching/separationlogic.md
similarity index 94%
rename from research/separationlogic.md
rename to teaching/separationlogic.md
index 5fe90f908037e9894d5af75fd14623660d0fc547..8902fa4001ec71a784a19d7f998cb63c470499fa 100644
--- a/research/separationlogic.md
+++ b/teaching/separationlogic.md
@@ -2,6 +2,7 @@
title: Separation Logic
project_id: sl
menu: true
+parent_menu: Teaching
menu_order: 5
---
@@ -42,14 +43,14 @@ Feedback: Monday 21st of November
Exam: 11th week
-Recommended Reading: Mike Gordon has some excellent notes on [Hoare logic](http://www.cl.cam.ac.uk/~mjcg/Teaching/2011/Hoare/Notes/Notes.pdf), which briefly touches on separation logic in the last chapter.
+Recommended Reading: Mike Gordon has some [excellent notes on Hoare logic](http://www.cl.cam.ac.uk/~mjcg/Teaching/2011/Hoare/Notes/Notes.pdf), which briefly touches on separation logic in the last chapter.
Two good books on Hoare logic are: Logic in Computer Science: Modelling and Reasoning about Systems, Michael Huth and Mark Ryan, CUP, 2004; and The Formal Semantics of Programming Languages: an Introduction, Glynn Winskel, MIT Press, 1993.
Most of the work on separation logic is in research papers.
Excellent introductions to separation logic include: O'Hearn, Reynolds and Yang's paper on [Local Reasoning about Programs that Alter Data Structures](http://www0.cs.ucl.ac.uk/staff/p.ohearn/papers/localreasoning.pdf), CSL 2001, and John Reynolds' undergraduate course notes on separation logic and survey paper [Separation Logic: A Logic for Shared Mutable Data Structures](https://www.cs.cmu.edu/~jcr/seplogic.pdf), LICS 2002, both found on Reynolds' homepage.
Andrew Appel has published a book on Program Logics for Certified Compilers, CUP 2014 (a copy is available in the [library](http://www.imperial.ac.uk/admin-services/library/)).
-Papers describing tool techniques include: [Symbolic Execution with Separation Logic](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.64.2006&rep=rep1&type=pdf), Berdine, Calcagno, O'Hearn, APLAS'05; [A Local Shape Analysis based on Separation Logic](http://www.eecs.qmul.ac.uk/~ddino/papers/localshape.pdf), Distefano, O'Hearn, Yang, TACAS 2006; and Compositional Shape Analysis by Means of Bi-abduction, Calcagno, Distefano, O'Hearn, Yang, JACM 2011.
+Papers describing tool techniques include: [Symbolic Execution with Separation Logic](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.64.2006&rep=rep1&type=pdf), Berdine, Calcagno, O'Hearn, APLAS'05; [A Local Shape Analysis based on Separation Logic](http://www.eecs.qmul.ac.uk/~ddino/papers/localshape.pdf), Distefano, O'Hearn, Yang, TACAS 2006; and [Compositional Shape Analysis by Means of Bi-abduction](http://www0.cs.ucl.ac.uk/staff/p.ohearn/papers/jacm-abduction-webversion.pdf), Calcagno, Distefano, O'Hearn, Yang, JACM 2011.
The initial paper on concurrent separation logic is [Resources, Concurrency and Local Reasoning](http://www0.cs.ucl.ac.uk/staff/p.ohearn/papers/concurrency.pdf), O'Hearn, TCS, 2007, and is worth a read.
The survey paper [Steps in Modular Specifications of Concurrent Modules](https://www.doc.ic.ac.uk/~pg/papers/mfps15.pdf), da Rocha Pinto, Dinsdale-Young, Gardner, MFPS 2015, describes some modern developments in concurrent separation logics.