Ayberk Tosun

formal-topology-in-UF. Formal Topology in Univalent Foundations (WIP).

sequents. Proof search for intuitionistic propositional logic using Dyckhoff's LJT.

grammar-inference. Learning rigid grammars in Haskell.

simplc. A tiny compiler for a security-typed imperative language with a formalised proof of noninterference-preservation.

sml-system-t. SML implementation of System T from PFPL.

Mini-TT. A tiny implementation of dependent types.

pixs. An image-processing library for Haskell.

sml-system-f. An implementation of System F, as described in PFPL.

abt. Ocaml port of CMU's ABT library (with various modifications).

chi. A minimal language with a self-interpreter.

agda-github-action. A GitHub action for typechecking Agda code.

gstts-formal-topology-talk. Slides for a talk given at the Gothenburg-Stockholm Type Theory Seminar.

linear-diophantine. An implementation of Contejean and Devie's algorithm for solving linear diophantine equations.

rafine. λ-calculus with ⊏, ≤, ∧, ∨.

AC-unification. Unification modulo associativity and commutativity.

tinyrw. A toy language based on rewriting using code from Baader and Nipkow.

agda-brzozowski. [WIP] Brzozowski's DFA minimization algorithm in Agda.

CFG-random. Generate random strings from a given CFG.

agda-logical-relations. Some experiments with logical relations in Agda.

resolution. A tiny implementation of logical resolution.

chalmers-msc-thesis-template. Template for master's theses at Chalmers. *Work in progress!*

turnstile. Proof translations from English to proof assistants.

GF-summer-school. Code and notes from the fifth GF summer school.

deasciifier. Deniz Yüret's Turkish deasciifier in Swift.

type-theory-turkish-dictionary.

turkish-pos-tagger. Part-of-speech tagging of Turkish, using hidden markov models.

msc-thesis. TeX

2048. Graphical 2048 in Python.

sml-colors. Make text look nice.

LamPi. Messing around with dependent types.

sml-redprl. Decisively Smash the Formalist Clique!—The People's Refinement Logic

notes-on-choice-sequences. Notes to myself as I am reading Troelstra's “Choice Sequences”.

twelf-playground. Toying with Twelf.

complexity-for-logicians. Notes from a mini course by Anupam Das.

DAT235.

docker-agda. Dockerfile

aspell-tr. Common Workflow Language

GF-twelf. Translate Twelf to other stuff—implemented in GF.

natural-sciences-forest. My forest for natural sciences, built using forester.

sml-cyk. [WIP] SML implementation of the Cocke-Kasami-Younger algorithm.

GFSS-5-presentation. Final presentation for the fifth GF summer school.

twelf-system-t. System T in Twelf.

pfm-exercises. Exercises from Paul Taylor's PFM.

TAPL. Notes and exercises from “Types and Programming Languages” by Pierce.