Weyl's Predicative Classical Mathematics as a Logic-Enriched Type Theory
What Causes a System to Satisfy a Specification?
What is a categorical model of the differential and the resource lambda-calculi?
What's Decidable About Sequences?
Why Would You Trust B?
Word Automaticity of Tree Automatic Scattered Linear Orderings Is Decidable
XCB, the Last of the Shortest Single Axioms for the Classical Equivalential Calculus
XNMR: A tool for knowledge bases exploration
YAPA: A generic tool for computing intruder knowledge
Yet Another Deep Embedding of B:Extending de Bruijn Notations
Yet Another Efficient Unification Algorithm
Yet another normalisation proof for Martin-Lof's logical framework--Terms with correct arities are strongly normalising