 Cayenne (programming language)

Cayenne is a dependently typed functional programming language created by Lennart Augustsson in 1998, making it one of the earliest dependently typed programming languages (as opposed to proof assistants or logical frameworks).A notable design decision is that the language allows unbounded recursive functions to be used on the type level, making type checking undecidable.