| 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 |
