a |

automata-theoretic decision technique | Tableau-Like Automata-Based Axiomatization for Propositional Linear Temporal Logic |

b |

Boolean BI | Towards a Cut-free Sequent Calculus for Boolean BI |

c |

cut elimination | Towards a Cut-free Sequent Calculus for Boolean BI |

d |

data accessibility | A Multi-Modal Dependent Type Theory for Representing Data Accessibility in a Network |

Distributed and Staged Computing | A Multi-Modal Dependent Type Theory for Representing Data Accessibility in a Network |

h |

Hoare logic | A Developer-oriented Hoare Logic |

Hoare-style Logic | A simple proof system for lock-free concurrency |

i |

Imperative core calculus | A simple proof system for lock-free concurrency |

l |

lightweight separation | A Developer-oriented Hoare Logic |

lock-free algorithms | A simple proof system for lock-free concurrency |

m |

Modal Type Theory | A Multi-Modal Dependent Type Theory for Representing Data Accessibility in a Network |

model checking | Tableau-Like Automata-Based Axiomatization for Propositional Linear Temporal Logic |

mu-calculus | A Proof System for Reasoning about Probabilistic Concurrent Processes Tableau-Like Automata-Based Axiomatization for Propositional Linear Temporal Logic |

p |

Probabilistic concurrent processes | A Proof System for Reasoning about Probabilistic Concurrent Processes |

Propositional Linear Temporal Logic | Tableau-Like Automata-Based Axiomatization for Propositional Linear Temporal Logic |

s |

separation logic | A simple proof system for lock-free concurrency |

sequent calculus | Towards a Cut-free Sequent Calculus for Boolean BI |

u |

understandable verification conditions | A Developer-oriented Hoare Logic |