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 |