wilbowma/experimenting-with-redex wilbowma/experimenting-with-redex

  • Stars
    star
    10
  • Rank 1,807,489 (Top 36 %)
  • Language
    Racket
  • License
    Other
  • Created about 5 years ago
  • Updated over 2 years ago
Twitter logo Share LinkedIn logo Share Facebook logo Share
wilbowma/experimenting-with-redex
github

wilbowma

Reviews

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

Repository Details

A Redex tutorial with a focus on how to do work in Redex

More Repositories

1

cur

A less devious proof assistant
Racket
220
star
2

pl-thesaurus

89
star
3

mttex

A LaTeX package for formatting meta-theory.
TeX
46
star
4

cic-redex

A Redex model of CIC as specified in Chapter 4 of the Coq reference manual.
Racket
32
star
5

dissertation

The source for "Compiling with Dependent Types" (my dissertation)
TeX
30
star
6

scribble-minted

A scribble library for using pygmentize
Racket
16
star
7

multi-lang-comp

a compiler from a lambda language to an assembly language, as a rewrite system
TeX
16
star
8

scribble-bettergrammar

A Scribble library for typesetting grammars better
Racket
15
star
9

scribble-coq

Because why wouldn't you want to typeset Coq in Scribble?
Racket
10
star
10

cur-control

An implementation of control operators for Cur.
Racket
6
star
11

tekkit-on-demand

Shell
6
star
12

the-unhinged-schemer

Racket
6
star
13

infernalize

Racket
5
star
14

llm-lang

An LLM-first programming language.
Racket
5
star
15

compiler-theory

Racket
5
star
16

scheme-site-template

A small website template system using R6RS scheme.
Scheme
5
star
17

cpanel-ddns

A script to automatically edit the ZoneEdit record on CPanel, allowing you to create your own DDNS server.
Perl
4
star
18

ubc-procmail

My UBC procmailrc setup
Python
4
star
19

ecc-redex

A model of Luo's ECC in Redex
Racket
4
star
20

deftech

A LaTeX implementation of Scribble's deftech and tech macros.
TeX
3
star
21

agda-experiments

Some experiments with modeling in Agda
Agda
3
star
22

pgmp

The source code for Profiled-Guided Meta-Programming (PLDI 2015)
Racket
2
star
23

dep-types-101

Some models of dependent types
Racket
2
star
24

ubc-letter-template

A template for UBC letters
TeX
2
star
25

who-self-phishes-the-self-phishers

2
star
26

crash-coq

An example of a linking error triggering a segfault when linking extracted Coq code to OCaml.
OCaml
2
star
27

cunittest

Python's unittest library, with threads.
Python
1
star
28

s3ql-rotating-snapshots

Shell
1
star
29

caldav-infer-freebusy

A Python script to generate a free/busy iCalendar from a server that doesn't support free/busy requests
Python
1
star
30

tfp2019-website

TFP 2019 website source
Racket
1
star
31

simply-typed-proofs

Racket
1
star
32

ccv-scrbl

a WIP DSL in Scribble for generating CCV
Racket
1
star
33

fib-lang

A DSL for fibonacci numbers
Racket
1
star
34

retex

A pacakge for Redex that looks like LaTeX
Racket
1
star