Idris, a general-purpose dependently typed programming language: Design and implementation
From MaRDI portal
Publication:5398331
DOI10.1017/S095679681300018XzbMATH Open1295.68059OpenAlexW2145108549WikidataQ56228328 ScholiaQ56228328MaRDI QIDQ5398331FDOQ5398331
Authors: 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
Recommendations
- A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family
- The Implicit Calculus of Constructions as a Programming Language with Dependent Types
- Idealized coinductive type systems for imperative object-oriented programs
- Selected papers from dependently typed programming 2010 -- overview
- scientific article; zbMATH DE number 1670486
- A tutorial implementation of a dependently typed lambda calculus
Cites Work
- Inductive families
- 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
- The Zipper
- \textsc{OutsideIn(X)}: modular type inference with local assumptions
- The view from the left
- Proceedings of the 15th ACM SIGPLAN international conference on Functional programming
Cited In (37)
- Eliminating dependent pattern matching without K
- Adding Negation to Lambda Mu
- Cogent: uniqueness types and certifying compilation
- I got plenty o' nuttin'
- Proof-relevant Horn clauses for dependent type inference and term synthesis
- Higher-order games with dependent types
- \texttt{slepice}: towards a verified implementation of type theory in type theory
- Visible type application
- Contributions to a computational theory of policy advice and avoidability
- Auto in Agda. Programming proof search using reflection
- Automatically proving equivalence by type-safe reflection
- On the correctness of monadic backward induction
- The essence of ornaments
- Title not available (Why is that?)
- Typed syntactic meta-programming
- Irdis
- A trustful monad for axiomatic reasoning with probability and nondeterminism
- Programming up to congruence
- Congruence closure in intensional type theory
- Elaborator reflection: extending Idris in Idris
- A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading
- \(\Pi \Sigma \): dependent types without the sugar
- Integrating induction and coinduction via closure operators and proof cycles
- A tutorial implementation of a dependently typed lambda calculus
- Cubical Agda: a dependently typed programming language with univalence and higher inductive types
- Implementing type theory in higher order constraint logic programming
- The Implicit Calculus of Constructions as a Programming Language with Dependent Types
- Guarded dependent type theory with coinductive types
- Dependently typed programming in Agda
- Uniqueness types for efficient and verifiable aliasing-free embedded systems programming
- Elaborating dependent (co)pattern matching: no pattern left behind
- A simple type-theoretic language: Mini-TT
- Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic
- Hammer for Coq: automation for dependent type theory
- Doo bee doo bee doo
- A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
- On the bright side of type classes: instance arguments in Agda
Uses Software
This page was built for publication: Idris, a general-purpose dependently typed programming language: Design and implementation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5398331)
