We derive an intuitionistic version of G\" odel-L\" ob modal logic ($\sf {GL} $) in the style of
Simpson, via proof theoretic techniques. We recover a labelled system, $\sf {\ell IGL} $, by …

We describe the categorical semantics for a simply typed variant and a simplified
dependently typed variant of Cocon, a contextual modal type theory where the box modality …

There have been investigations into type-theoretic foundations for metaprogramming,
notably Davies and Pfenning's (2001) treatment in S4 modal logic, where code evaluating to …

We describe a category-theoretic semantics for a simply typed variant of Cocon, a contextual
modal type theory where the box modality mediates between the weak function space that is …

The cut-elimination procedure for the provability logic is known to be problematic: a L\" ob-
like rule keeps cut-formulae intact on reduction, even in the principal case, thereby …

Intensionality is a phenomenon that occurs in logic and computation. In the most general
sense, a function is intensional if it operates at a level finer than (extensional) equality. This …

Functors with an instance of the Traversable type class can be thought of as data structures
which permit a traversal of their elements. This has been made precise by the …

Theorem provers such as Lean and Coq use metaprogramming to automate proof-writing,
making the process less tedious. These theorem provers are all variations of Martin-Löf's …

We derive an intuitionistic version of Gödel-Löb modal logic (GL) in the style of Simpson, via
proof theoretic techniques. We recover a labelled system, ℓIGL, by restricting a non …

Noninterference properties state that data does not flow in an undesirable manner, eg from a
high-security to a low-security setting. Within programming languages noninterference is …