Type Patterns: Pattern Matching on Shape-Carrying Array Types
A logical relations model of a minimal type theory with bounded first-class universe levels mechanized in Lean.
Logical relation for predicative CC omega with booleans and an intensional identity type
prototype implementation of a dependently-typed language with an extendable constraints and accompanying materials
Functional Pearl: Witness Me — Constructive Arguments Must Be Guided with Concrete Witness
Source code for the paper "Specifying and Verifying a Transformation of Recursive Functions into Tail-Recursive Functions"
The Agda Universal Algebra Library (UALib) is a library of types and programs (theorems and proofs) that formalizes the foundations of universal algebra in dependent type theory using the Agda proof assistant language.
"Dependent Types for Software Engineers" - Report for the Seminar "Program Analysis and Transformation" in HS2020 about dependent types.
Malfunction backend for Idris with a FFI to OCaml
My now-completed Master's thesis.
A LUG Talk about Idris, a general purpose language with dependent types.
Calvin Talks Types
Add a description, image, and links to the dependent-types topic page so that developers can more easily learn about it.
To associate your repository with the dependent-types topic, visit your repo's landing page and select "manage topics."