Dijkstra Monads for All This paper proposes a general semantic framework for verifying programs with arbitrary monadic sideeffects using Dijkstra monads, which we define as monadlike structures indexed by a specification monad. We prove that any monad morphism between a computational monad and a specification monad gives rise to a Dijkstra monad, which provides great flexibility for obtaining Dijkstra monads tailored to the verification task at hand. We moreover show that a large variety of specification monads can be obtained by applying monad transformers to various base specification monads, including predicate transformers and Hoarestyle pre and postconditions. For simplifying the task of defining correct monad transformers, we propose a language inspired by Moggiu0027s monadic metalanguage that is parameterized by a dependent type theory. We also develop a notion of Plotkin and Poweru0027s algebraic operations for Dijkstra monads, together with a corresponding notion of effect handlers. We implement our framework in both Coq and F*, and illustrate that it supports a wide variety of verification styles for effects such as partiality, exceptions, nondeterminism, state, and inputoutput.

A Path To DOT: Formalizing FullyPathDependent Types The Dependent Object Types (DOT) calculus aims to formalize the Scala programming language with a focus on pathdependent types  types such as x.a_1dots a_n.T that depend on the runtime value of a path x.a_1dots a_n to an object. Unfortunately, existing formulations of DOT can model only types of the form x.A which depend on variables rather than general paths. This restriction makes it impossible to model nested module dependencies. Nesting small components inside larger ones is a necessary ingredient of a modular, scalable language. DOTu0027s variable restriction thus undermines its ability to fully formalize a variety of programminglanguage features including Scalau0027s module system, family polymorphism, and covariant specialization.  :109,paper presents the pDOT calculus, which generalizes DOT to support types that depend on paths of arbitrary length, as well as singleton types to track path equality. We show that naive approaches to add paths to DOT make it inherently unsound, and present necessary conditions for such a calculus to be sound. We discuss the key changes necessary to adapt the techniques of the DOT soundness proofs so that they can be applied to pDOT. Our :109,paper comes with a Coqmechanized typesafety proof of pDOT. With support for paths of arbitrary length, pDOT can realize DOTu0027s full potential for formalizing Scalalike calculi.