Bob Atkey

sott. Simplified Observational Type Theory

modulog. A Datalog implementation with an OCaml inspired module system

CS316-19. The 2019/2020 edition of Strathclyde's CS316 Functional Programming course

ocamlmvc. An MVC library for writing interactive webpages in OCaml

CS316-18. The 2018-19 edition of Strathclyde's CS316 "Functional Programming" course

agda-metric-reals. Agda

foveran. A Dependently Typed Programming Language

unboxed. Unboxed arrays for OCaml

CS316-2022. Materials for the 2022-2023 edition of CS316 "Functional Programming"

CS316-2020. The 2020-21 Edition of CS316 "Functional Programming" @ the University of Strathclyde

system-f-parametricity-model. A Model of Relationally Parametric System F in Coq

CS316-17. The 2017-18 edition of Strathclyde's CS316 "Functional Programming" course

interactive-natural-deduction. An editor for interactively building natural deduction proofs

sorting-types. Typed DSLs for sorting

playtime. An OCaml EDSL for describing and solving strategic games

authenticated-data-structures. An implementation of generic authenticated data structures in OCaml

algebraically-indexed-types. Repository for documents and experiments to do with algebraically-indexed types

semantic-cut-elimination. Cut-elimination by Semantic Means

qtt-models. Formalisations of interesting models of QTT

Forvie. Some Programming Language Description and Processing Tools in Haskell

array-mapped-trie. An Array Mapped Trie implementation in OCaml

acfg-parser. Parser for Active Context Free Grammars

pretty-monospace. An OCaml pretty-printing library for monospaced text

ppx-monoid. OCaml

CS316-2021. The 2021/22 edition of Strathclyde's Functional Programming course in Haskell

ppx-markdown. OCaml PPX extension for including markdown in OCaml source files

approx-diff. Approximation as Differentiation

polly. A simple language for services

coqjvm. Coq executable semantics and resource verifier

clocked-types.

parser-combinators-intro. Slides for an introductory talk on Parser Combinators

opam-repository. Main public package repository for OPAM, the source package manager of OCaml.

Inductors. Notes and implementations of inductors

ulmus. Ulmus

camlcheck. An OCaml QuickCheck clone

access_log. OCaml