Idris, a general-purpose dependently typed programming language: Design and implementation

DOI10.1017/S095679681300018XzbMath1295.68059OpenAlexW2145108549WikidataQ56228328 ScholiaQ56228328MaRDI QIDQ5398331

Edwin Brady

Publication date: 27 February 2014

Published in: Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s095679681300018x

zbMATH Keywords

implementationfunctional programming languagesyntaxIdris

Mathematics Subject Classification ID

Theory of programming languages (68N15) Functional programming and lambda calculus (68N18)

Related Items (26)

Automatically proving equivalence by type-safe reflection ⋮ I Got Plenty o’ Nuttin’ ⋮ Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis ⋮ Hammer for Coq: automation for dependent type theory ⋮ Contributions to a computational theory of policy advice and avoidability ⋮ Auto in Agda ⋮ Higher-order games with dependent types ⋮ Adding Negation to Lambda Mu ⋮ Elaborating dependent (co)pattern matching: No pattern left behind ⋮ Doo bee doo bee doo ⋮ Eliminating dependent pattern matching without K ⋮ The essence of ornaments ⋮ A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading ⋮ Unnamed Item ⋮ A trustful monad for axiomatic reasoning with probability and nondeterminism ⋮ Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic ⋮ Visible Type Application ⋮ Guarded Dependent Type Theory with Coinductive Types ⋮ Congruence Closure in Intensional Type Theory ⋮ Irdis ⋮ Integrating induction and coinduction via closure operators and proof cycles ⋮ Cubical Agda: A dependently typed programming language with univalence and higher inductive types ⋮ A type- and scope-safe universe of syntaxes with binding: their semantics and proofs ⋮ Cogent: uniqueness types and certifying compilation ⋮ On the correctness of monadic backward induction ⋮ \texttt{slepice}: towards a verified implementation of type theory in type theory

Uses Software

• Coq
• Haskell
• Idris

Cites Work

• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Unification under a mixed prefix
• Inductive families
• The Zipper
• The view from the left
• <scp>OutsideIn(X)</scp>Modular type inference with local assumptions
• Proceedings of the 15th ACM SIGPLAN international conference on Functional programming

This page was built for publication: Idris, a general-purpose dependently typed programming language: Design and implementation