Towards a practical programming language based on dependent type theory

2007

361 citations recorded by the source corpus.

View Paper: https://www.semanticscholar.org/paper/345b2a3a2e99221f180b752b06b7f229993f5c9a

Citations in the corpus

• Dependently typed programming in Agda (2009, unknown): “My thesis [5] contains more of the technical and theoretical details behind Agda, as well as some programming examples.”
• Dependent types and multi-monadic effects in F* (2016, unknown): “Agda offers two termination checkers.”
• Refinement types for Haskell (2014, unknown): ““Full” dependently typed systems like Coq [5], Agda [24], and Idris [7] typically use structural checks where recursion is allowed on sub-terms of ADTs to ensure that all terms terminate.”
• A Brief Overview of Agda - A Functional Language with Dependent Types (2009, unknown): “There is also a link to Norell’s PhD thesis [14] with a language definition and detailed discussions of the features of Agda.”