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

Questions & Answers
,
1

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?

2

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/

1 Like