# Is there any Redex implementation of a very minimal dependently typed Lambda Calculus core? Something like Elaboration-Zoo-02

**URL:** <https://racket.discourse.group/t/is-there-any-redex-implementation-of-a-very-minimal-dependently-typed-lambda-calculus-core-something-like-elaboration-zoo-02/2957>\
**Category:** Questions & Answers\
**Tags:** question, redex\
**Created:** [June 8, 2024, 5:58pm UTC](https://racket.discourse.group/t/is-there-any-redex-implementation-of-a-very-minimal-dependently-typed-lambda-calculus-core-something-like-elaboration-zoo-02/2957 "2024-06-08T17:58:36Z")\
**Posts on this page:** 2\
**Page:** 1

<div class="post-metadata">

**Author:** ![B0B](https://avatars.discourse-cdn.com/v4/letter/b/34f0e0/32.png) [@B0B](https://racket.discourse.group/u/B0B)\
**Post date:** [June 8, 2024, 5:58pm UTC](https://racket.discourse.group/t/is-there-any-redex-implementation-of-a-very-minimal-dependently-typed-lambda-calculus-core-something-like-elaboration-zoo-02/2957/1 "2024-06-08T17:58:36Z")

</div>

I'd like to prototype/play-around-with a dependently typed language.

I'm very new to Racket, but would like to use Redex (or any similar tool) to define some decent typing and evaluation rules.

I've gone through the two tutorials in the manual, but a lot of details seem trickier to get right than I was hoping for. For instance, α/β/η-conversion/equivalence: I can more or less follow the ones implemented in the tutorial, but I doubt I could write a working version myself.

Is there any simple implementation of a very minimal, dependently typed lambda calculus I could start off from?

---

<div class="post-metadata">

**Author:** ![jbclements](https://yyz2.discourse-cdn.com/free1/user_avatar/racket.discourse.group/jbclements/32/11_2.png) [@jbclements](https://racket.discourse.group/u/jbclements)\
**Post date:** [June 8, 2024, 10:04pm UTC](https://racket.discourse.group/t/is-there-any-redex-implementation-of-a-very-minimal-dependently-typed-lambda-calculus-core-something-like-elaboration-zoo-02/2957/2 "2024-06-08T22:04:48Z")

</div>

This is not redex-related at all, but have you seen Prabahkar Ragde's flânerie called "Logic and Computing Intertwined"? It walks through building a simplified dependently-typed LC engine in Racket, before eventually transitioning to Agda and Coq:

[https://cs.uwaterloo.ca/~plragde/flaneries/LACI/](https://cs.uwaterloo.ca/~plragde/flaneries/LACI/)