natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory
Haskell is a typed functional programming language. It is named after Haskell Brooks Curry?.
There is a category $\mathbf{Haskell}$ whose objects are Haskell types and whose morphisms are Haskell functions.
Haskell is famous for its use of monads (in computer science) acting on this category.
Languages similar to Haskell but refining it from plain type theory to dependent type theory include
A wiki platform based on Haskell, running texmath
Haskell, language and library specification, wiki
The use of Haskell in mathematics is discussed in the following references.
haskellwiki, Haskell and mathematics
category theory, in haskellwiki, wiki
Jan van Eijck, The Haskell Road to Logic, Maths and Programming