# Mini-TT in Racket

**URL:** https://racket.discourse.group/t/mini-tt-in-racket/2007
**Category:** Show & Tell
**Tags:** typed-racket
**Created:** [June 13, 2023, 5:57pm UTC](https://racket.discourse.group/t/mini-tt-in-racket/2007 "2023-06-13T17:57:34Z")
**Posts on this page:** 1
**Page:** 1

<div class="post-metadata">

### Author: ![hanleyc01](https://yyz2.discourse-cdn.com/free1/user_avatar/racket.discourse.group/hanleyc01/32/1206_2.png) [@hanleyc01](https://racket.discourse.group/u/hanleyc01)
#### Post date: [June 13, 2023, 5:57pm UTC](https://racket.discourse.group/t/mini-tt-in-racket/2007/1 "2023-06-13T17:57:34Z")

</div>

I posted this on Discord, but I'm very proud of this, even if it is largely just a translation of the implementation provided by Coquand et al.'s [Mini-TT](https://www.cambridge.org/core/books/abs/from-semantics-to-computer-science/simple-typetheoretic-language-minitt/21451A12E2E24A1F51C82421B066824A).

Here's the repo: [GitHub - hanleyc01/rkttt](https://github.com/hanleyc01/rkttt)

It's largely undocumented, but the main algorithm is in `tc.rkt` - I'm working on some documentation that helps with understanding exactly how the program works, but either way implementing it has helped me a lot in understanding bidirectional typechecking 🙂.

If you do look at it, I apologize for if anything is ugly or unreadable, or if there are some dead ends that don't lead anywhere (`/nanopass-experiment/`, e.g.). Either way, this was the most fun I've had working on a project, and some of the most fun I've had playing with my computer ever.