A Self-Taught Course in Automated Reasoning using Haskell


Frank Pfenning getting in the smart contract game??

Resource-Aware Session Types for Digital Contracts

Byrne’s Euclid

A reproduction of Oliver Byrne’s celebrated work from 1847 plus interactive diagrams, cross references, and posters designed by Nicholas Rougeux


Fast Downward

Fast Downward is a classical planning system based on heuristic search. It can deal with general deterministic planning problems encoded in the propositional fragment of PDDL2.2, including advanced features like ADL conditions and effects and derived predicates (axioms). Like other well-known planners such as HSP and FF, Fast Downward is a progression planner, searching the space of world states of a planning task in the forward direction. However, unlike other PDDL planning systems, Fast Downward does not use the propositional PDDL representation of a planning task directly. Instead, the input is first translated into an alternative representation called multi-valued planning tasks, which makes many of the implicit constraints of a propositional planning task explicit. Exploiting this alternative representation, Fast Downward uses hierarchical decompositions of planning tasks for computing its heuristic function, called the causal graph heuristic, which is very different from traditional HSP-like heuristics based on ignoring negative interactions of operators.

Fast Downward home page

Solving Planning Problems with Fast Downward and Haskell

Algebra of Programming

As If Summoned from the Void: The Life of Alexandre Grothendieck

Towards Live Programming Environments for Statically Verified JavaScript

In particular, the Javascript Program Verification section.

Real Induction

Commutative Monads, Diagrams, and Knots

Presentation by Dan Piponi


A Semigroupoid is a Category without the requirement of identity arrows for every object in the category.

A Category is any Semigroupoid for which the Yoneda lemma holds.

Nada Amin metaprogramming lecture notes

Pfenning courses

Lawvere theories

A contravariant functor turns coproducts into products and injections to projections

Morphisms between Lawvere theories encapsulate the idea of the interpretation of one theory inside another.

The key to understand Lawvere theories is to realize that one such theory generalizes a lot of individual algebras that share the same structure. For instance, the Lawvere theory of monoids describes the essence of being a monoid. It must be valid for all monoids. A particular monoid becomes a model of such a theory.

K Framework


defined using configurations, computations and rules

  • Configurations organize the state in units called cells, which are labeled and can be nested.
  • Computations carry computational meaning as special nested list structures sequentializing computational tasks, such as fragments of program.
  • K (rewrite) rules make it explicit which parts of the term they read-only, write-only, read-write, or do not care about. This makes K suitable for defining truly concurrent languages even in the presence of sharing. Computations are like any other terms in a rewriting environment: they can be matched, moved from one place to another, modified, or deleted. This makes K suitable for defining control-intensive features such as abrupt termination, exceptions, concurrency or call/cc.

BaKoMa TeX

“True WYSIWYG LaTeX System”. Impressive-looking TeX editor.

Automatic investing

A framework for improving error messages in dependently-typed languages

Dependently-typed programming languages provide a powerful tool for establishing code correctness. However, it can be hard for newcomers to learn how to employ the advanced type system of such languages effectively. For simply-typed languages, several techniques have been devised to generate helpful error messages and suggestions for the programmer. We adapt these techniques to dependently-typed languages, to facilitate their more widespread adoption. In particular, we modify a higher-order unification algorithm that is used to resolve and type-check implicit arguments. We augment this algorithm with replay graphs, allowing for a global heuristic analysis of a unification problem-set, error-tolerant typing, which allows type-checking to continue after errors are found, and counter-factual unification, which makes error messages less affected by the order in which types are checked. A formalization of our algorithm is presented with an outline of its correctness. We implement replay graphs, and compare the generated error messages to those from existing languages, highlighting the improvements we achieved.

Quantilizers: A Safer Alternative to Maximizers for Limited Optimization

In the field of AI, expected utility maximizers are commonly used as a model for idealized agents. However, expected utility maximization can lead to unintended solutions when the utility function does not quantify everything the operators care about: imagine, for example, an expected utility maximizer tasked with winning money on the stock market, which has no regard for whether it accidentally causes a market crash. Once AI systems become sufficiently intelligent and powerful, these unintended solutions could become quite dangerous. In this paper, we describe an alternative to expected utility maximization for powerful AI systems, which we call expected utility quantilization. This could allow the construction of AI systems that do not necessarily fall into strange and unanticipated shortcuts and edge cases in pursuit of their goals.

Jane Street paper on accelerating self-play learning



By introducing several new Go-specific and non-Go-specific techniques along with other tuning, we accelerate self-play learning in Go. Like AlphaZero and Leela Zero, a popular open-source distributed project based on AlphaZero, our bot KataGo only learns from neural net Monte-Carlo tree-search self-play. With our techniques, in only a week with several dozen GPUs it achieves a likely strong pro or perhaps just-super-human level of strength. Compared to Leela Zero, we estimate a roughly 5x reduction in self-play computation required to achieve that level of strength, as well as a 30x to 100x reduction for reaching moderate to strong amateur levels. Although we so far have not tested in longer runs, we believe that our techniques hold promise for future research.

mini version of Deep Learning for Protein Structure Prediction inspired by DeepMind AlphaFold algorithm

Dead simple haskell travis settings for cabal and stack

Relevant and substructural logics