17 citations · 35 across the 10 of their papers we have counts for
5 papers · 1 filter
A modest proposal: explicit support for foundational pluralism
Martin Berger, Dominic P. Mulligan
Whilst mathematicians assume classical reasoning principles by default they often context switch when working, restricting themselves to various forms of subclassical reasoning. Th…
A program logic for fresh name generation
Harold Pancho Eliott, Martin Berger
We present a program logic for Pitts and Stark's ν-calculus, an extension of the call-by-value simply-typed λ-calculus with a mechanism for the generation of fresh names. Names can…
Cathoristic logic: A modal logic of incompatible propositions
Richard Prideaux Evans, Martin Berger
Cathoristic logic is a multi-modal logic where negation is replaced by a novel operator allowing the expression of incompatible sentences. We present the syntax and semantics of th…
Program Logics for Homogeneous Generative Run-Time Meta-Programming
Martin Berger, Laurence Tratt
This paper provides the first program logic for homogeneous generative run-time meta-programming---using a variant of MiniML by Davies and Pfenning as its underlying meta-programmi…
Logical Reasoning for Higher-Order Functions with Local State
Nobuko Yoshida, Kohei Honda, Martin Berger
We introduce an extension of Hoare logic for call-by-value higher-order functions with ML-like local reference generation. Local references may be generated dynamically and exporte…