ayberkt/TAPL

Stars
1
Language
Haskell
License
BSD 3-Clause "New...
Created almost 9 years ago
Updated over 8 years ago

ayberkt/TAPL

ayberkt

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

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

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.

abt

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

sml-system-f

An implementation of System F, as described in PFPL.

agda-github-action

A GitHub action for typechecking Agda code.

chi

A minimal language with a self-interpreter.

notes-on-cut-elimination

Some notes and Twelf code on cut elimination.

rafine

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

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.

AC-unification

Unification modulo associativity and commutativity.

agda-brzozowski

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

CFG-random

Generate random strings from a given CFG.

tinyrw

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

chalmers-msc-thesis-template

Template for master's theses at Chalmers. *Work in progress!*

resolution

A tiny implementation of logical resolution.

deasciifier

Deniz Yüret's Turkish deasciifier in Swift.

turnstile

Proof translations from English to proof assistants.

Grammatical Framework

agda-logical-relations

Some experiments with logical relations in Agda.

system-t-normalization

Normlization proof of System T in Agda.

GF-summer-school

Code and notes from the fifth GF summer school.

Grammatical Framework

sml-colors

Make text look nice.

turkish-pos-tagger

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

LamPi

Messing around with dependent types.

msc-thesis

notes-on-choice-sequences

Notes to myself as I am reading Troelstra's “Choice Sequences”.

2048

Graphical 2048 in Python.

complexity-for-logicians

Notes from a mini course by Anupam Das.

twelf-playground

Toying with Twelf.

continuity-bibliography

[WIP] An annotated bibliography on the works on continuity principles in type theories.

sml-cyk

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

pfm-exercises

Exercises from Paul Taylor's PFM.

docker-agda

natural-sciences-forest

My forest for natural sciences, built using forester.

twelf-system-t

System T in Twelf.

aspell-tr

Common Workflow Language

DAT235

GFSS-5-presentation

Final presentation for the fifth GF summer school.

GF-twelf

Translate Twelf to other stuff—implemented in GF.

Grammatical Framework