Alex Gryzlov

sequent-calc-talk. Code for the "Logic, machines and sequent calculus" talk

sequent-calc. Experiments with sequent calculi

modal-types. Experiments with modal types

idris-linear. Experiments with linear types

opticui-elm-architecture. Elm arch guide in OpticUI

coherence-spaces. linear logic semantics

guarded-cm. Experiments with guarded recursion

rp-with-monix. Examples from "Reactive Programming with RxJava" in Monix

exp-subs. Explicit substitution calculi

dialectica. Dialectica translations

logrel-guarded. Guarded logical relations

idris-smtlib. SMT-LIB text interface for Idris

log-rels. Logical relations and normalisation

idris-trees. Trees in Idris

ipc-ssr. Weich's Intuitionistic Solver in SSReflect

blott-experiments. Experiments with dependent modal types

refutation. Refutation and paraconsistent calculi

idris-selective. Selective functors in Idris

think-bayes-idris. Think Bayes in Idris

resolution-ssr. Resolution in SSReflect

free-applicative. Free Applicative Functor

pfad-scala. Pearls of Functional Algorithm Design in Scala

language-redtt. VSCode plugin for redtt

guarded-absint. Guarded abstract interpretation

comonads. Scala

idris-datadata. Datatypes of datatypes

kanren. Port of miniKanren to Scala

unification-cm. unification algorithms in CuTT

idris-semidirect. Semidirect products for Idris

preger. Presburger solver

idris-functors. Functors

force-layout. PureScript

scalaz7-examples. Scala

poly-cm. Polynomials & interaction structures

idris-free. Free Monads and useful constructions to work with them

idris-vecspace. Abstract vector spaces in Idris

unification. unification algorithms in Idris

the-power-of-pi. Implementations of ideas in The Power of Pi.