Idris, a general-purpose dependently typed programming language: Design and implementation
From MaRDI portal
Publication:5398331
DOI10.1017/S095679681300018XzbMATH Open1295.68059OpenAlexW2145108549WikidataQ56228328 ScholiaQ56228328MaRDI QIDQ5398331FDOQ5398331
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
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
- <scp>OutsideIn(X)</scp>Modular type inference with local assumptions
- The view from the left
- Proceedings of the 15th ACM SIGPLAN international conference on Functional programming
Cited In (27)
- Eliminating dependent pattern matching without K
- Guarded Dependent Type Theory with Coinductive Types
- Adding Negation to Lambda Mu
- Cogent: uniqueness types and certifying compilation
- Higher-order games with dependent types
- \texttt{slepice}: towards a verified implementation of type theory in type theory
- Contributions to a computational theory of policy advice and avoidability
- Cubical Agda: A dependently typed programming language with univalence and higher inductive types
- I Got Plenty o’ Nuttin’
- Automatically proving equivalence by type-safe reflection
- Visible Type Application
- On the correctness of monadic backward induction
- The essence of ornaments
- Elaborating dependent (co)pattern matching: No pattern left behind
- Title not available (Why is that?)
- Auto in Agda
- Irdis
- A trustful monad for axiomatic reasoning with probability and nondeterminism
- A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading
- Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis
- Integrating induction and coinduction via closure operators and proof cycles
- Congruence Closure in Intensional Type Theory
- Uniqueness types for efficient and verifiable aliasing-free embedded systems programming
- 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
Uses Software
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 👍 👎
- Title not available (Why is that?) 👍 👎
- A Tutorial Implementation of a Dependently Typed Lambda Calculus 👍 👎
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)
