From the 1 of 4 linked papers with an AI index.
4 papers
Logical Foundations of Two-Sided Type Theory
Celia Mengyue Li, Steven Ramsay
The paper develops the logical basis of two‑sided type systems, introducing new systems (2λInt, 2λInt~ and 2λHOL) that correspond to bilateral logic and its extension with strong n…
A Complementary Approach to Incorrectness Typing
Celia Mengyue Li, Sophie Pull, Steven Ramsay
We introduce a new two-sided type system for verifying the correctness and incorrectness of functional programs with atoms and pattern matching. A key idea in the work is that type…
Bisimilarity in fresh-register automata
Andrzej S. Murawski, Steven J. Ramsay, Nikos Tzevelekos
Register automata are a basic model of computation over infinite alphabets. Fresh-register automata extend register automata with the capability to generate fresh symbols in order…
Effect Handlers for Programmable Inference
Minh Nguyen, Roly Perera, Meng Wang +1
Inference algorithms for probabilistic programming are complex imperative programs with many moving parts. Efficient inference often requires customising an algorithm to a particul…