ayberkt/GF-twelf ayberkt/GF-twelf

  • Stars
    star
    1
  • Language Grammatical Framework
  • License
    GNU General Publi...
  • Created about 7 years ago
  • Updated about 7 years ago
Twitter logo Share LinkedIn logo Share Facebook logo Share
ayberkt/GF-twelf
github

ayberkt

Reviews

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

Repository Details

Translate Twelf to other stuff—implemented in GF.

More Repositories

1

formal-topology-in-UF

Formal Topology in Univalent Foundations (WIP).
CSS
33
star
2

sequents

Proof search for intuitionistic propositional logic using Dyckhoff's LJT.
Standard ML
26
star
3

grammar-inference

Learning rigid grammars in Haskell.
Haskell
24
star
4

simplc

A tiny compiler for a security-typed imperative language with a formalised proof of noninterference-preservation.
Agda
14
star
5

sml-system-t

SML implementation of System T from PFPL.
Standard ML
11
star
6

Mini-TT

A tiny implementation of dependent types.
Standard ML
11
star
7

pixs

An image-processing library for Haskell.
Haskell
10
star
8

abt

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

sml-system-f

An implementation of System F, as described in PFPL.
Standard ML
9
star
10

agda-github-action

A GitHub action for typechecking Agda code.
Shell
7
star
11

chi

A minimal language with a self-interpreter.
OCaml
7
star
12

notes-on-cut-elimination

Some notes and Twelf code on cut elimination.
TeX
6
star
13

rafine

λ-calculus with ⊏, ≤, ∧, ∨.
Standard ML
5
star
14

gstts-formal-topology-talk

Slides for a talk given at the Gothenburg-Stockholm Type Theory Seminar.
TeX
5
star
15

linear-diophantine

An implementation of Contejean and Devie's algorithm for solving linear diophantine equations.
Scala
5
star
16

AC-unification

Unification modulo associativity and commutativity.
Scala
4
star
17

agda-brzozowski

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

CFG-random

Generate random strings from a given CFG.
Haskell
4
star
19

tinyrw

A toy language based on rewriting using code from Baader and Nipkow.
Standard ML
4
star
20

chalmers-msc-thesis-template

Template for master's theses at Chalmers. *Work in progress!*
TeX
3
star
21

resolution

A tiny implementation of logical resolution.
OCaml
3
star
22

deasciifier

Deniz Yüret's Turkish deasciifier in Swift.
Swift
3
star
23

turnstile

Proof translations from English to proof assistants.
Grammatical Framework
3
star
24

agda-logical-relations

Some experiments with logical relations in Agda.
Agda
3
star
25

system-t-normalization

Normlization proof of System T in Agda.
Agda
3
star
26

GF-summer-school

Code and notes from the fifth GF summer school.
Grammatical Framework
3
star
27

sml-colors

Make text look nice.
Standard ML
2
star
28

turkish-pos-tagger

Part-of-speech tagging of Turkish, using hidden markov models.
Haskell
2
star
29

LamPi

Messing around with dependent types.
OCaml
2
star
30

msc-thesis

TeX
2
star
31

notes-on-choice-sequences

Notes to myself as I am reading Troelstra's “Choice Sequences”.
TeX
2
star
32

2048

Graphical 2048 in Python.
Python
2
star
33

complexity-for-logicians

Notes from a mini course by Anupam Das.
CSS
2
star
34

twelf-playground

Toying with Twelf.
2
star
35

continuity-bibliography

[WIP] An annotated bibliography on the works on continuity principles in type theories.
TeX
1
star
36

sml-cyk

[WIP] SML implementation of the Cocke-Kasami-Younger algorithm.
Standard ML
1
star
37

pfm-exercises

Exercises from Paul Taylor's PFM.
TeX
1
star
38

docker-agda

Dockerfile
1
star
39

natural-sciences-forest

My forest for natural sciences, built using forester.
XSLT
1
star
40

twelf-system-t

System T in Twelf.
1
star
41

aspell-tr

Common Workflow Language
1
star
42

DAT235

1
star
43

GFSS-5-presentation

Final presentation for the fifth GF summer school.
TeX
1
star
44

TAPL

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