Package papers - Namespaces

• Control.DivideAndConquer

  The content of this module is based on the paper A Type-Based Approach to Divide-And-Conquer Recursion in Coq by Pedro Abreu, Benjamin Delaware, Alex Hubers, Christa Jenkins, J. Garret Morris, and Aaron Stump https://doi.org/10.1145/3571196 The original paper relies on Coq's impredicative Set axiom, something we don't have access to in Idris 2. We can however reproduce the results by ignoring the type levels
• Data.Container
• Data.Description.Regular

  The content of this module is based on the paper A Completely Unique Account of Enumeration by Cas van der Rest, and Wouter Swierstra https://doi.org/10.1145/3547636
• Data.Description.Indexed

  The content of this module is based on the paper A Completely Unique Account of Enumeration by Cas van der Rest, and Wouter Swierstra https://doi.org/10.1145/3547636
• Data.Enumerate

  The content of this module is based on the paper A Completely Unique Account of Enumeration by Cas van der Rest, and Wouter Swierstra https://doi.org/10.1145/3547636
• Data.Enumerate.Common
• Data.Enumerate.Indexed

  The content of this module is based on the paper A Completely Unique Account of Enumeration by Cas van der Rest, and Wouter Swierstra https://doi.org/10.1145/3547636
• Data.InductionRecursion.DybjerSetzer

  There are different flavours of induction-recursion. This is the one introduced in Dybjer and Setzer's paper: Indexed induction-recursion
• Data.INTEGER
• Data.Linear.Communications

  This module is based on the content of the functional pearl How to Take the Inverse of a Type by Daniel Marshall and Dominic Orchard
• Data.Linear.Diff

  This module is based on the content of the functional pearl How to Take the Inverse of a Type by Daniel Marshall and Dominic Orchard
• Data.Linear.Inverse

  This module is based on the content of the functional pearl How to Take the Inverse of a Type by Daniel Marshall and Dominic Orchard
• Data.ProofDelay

  The contents of this module are based on the paper Deferring the Details and Deriving Programs by Liam O'Connor https://doi.org/10.1145/3331554.3342605
• Data.Recursion.Free

  Module partially based on McBride's paper: Turing-Completeness Totally Free It gives us a type to describe computation using general recursion and functions to run these computations for a while or to completion if we are able to prove them total. The content of the Erased section is new. Instead of producing the domain/evaluation pair by computing a Dybjer-Setzer code we build a specialised structure that allows us to make the domain proof runtime irrelevant.
• Data.Tree.Perfect
• Data.Vect.Binary

  The content of this file is taken from the paper Heterogeneous Binary Random-access lists
• Data.W
• Language.IntrinsicScoping.Variables
• Language.IntrinsicScoping.TypeTheory

  The content of this module is based on the paper: A tutorial implementation of a dependently typed lambda calculus by Andres Löh, Conor McBride, and Wouter Swierstra NB: Unlike `Language.TypeTheory`, this is not a direct translation of the code in the paper but rather a more idiomatic solution.
• Language.IntrinsicTyping.ABT

  Abstract binding trees are a generic representation of terms over a given signature
• Language.IntrinsicTyping.Krivine

  The content of this module is based on the paper From Mathematics to Abstract Machine A formal derivation of an executable Krivine machine by Wouter Swierstra
• Language.IntrinsicTyping.SECD

  The content of this module is based on the MSc Thesis Coinductive Formalization of SECD Machine in Agda by Adam Krupička
• Language.IntrinsicTyping.STLCR

  The content of this module is based on the MSc Thesis Coinductive Formalization of SECD Machine in Agda by Adam Krupička
• Language.Tagless

  This module is based on the paper Dependent Tagless Final by Nicoals Biri
• Language.TypeTheory

  The content of this module is based on the paper: A tutorial implementation of a dependently typed lambda calculus by Andres Löh, Conor McBride, and Wouter Swierstra NB: The work is originally written in Haskell and uses unsafe features This is not how we would write idiomatic Idris code. Cf. Language.IntrinsicScoping.TypeTheory for a more idiomatic representation.
• Search.Auto

  The content of this module is based on the paper Auto in Agda - Programming proof search using reflection by Wen Kokke and Wouter Swierstra
• Search.Generator

  The content of this module is based on the paper Applications of Applicative Proof Search by Liam O'Connor https://doi.org/10.1145/2976022.2976030 The main difference is that we use `Colist1` for the type of generators rather than `Stream`. This allows us to avoid generating many duplicates when dealing with finite types which are common in programming (Bool) but even more so in dependently typed programming (Vect 0, Fin (S n), etc.).
• Search.HDecidable

  The content of this module is based on the paper Applications of Applicative Proof Search by Liam O'Connor https://doi.org/10.1145/2976022.2976030
• Search.Negation
• Search.Properties

  The content of this module is based on the paper Applications of Applicative Proof Search by Liam O'Connor https://doi.org/10.1145/2976022.2976030
• Search.CTL

  The content of this module is based on the paper Applications of Applicative Proof Search by Liam O'Connor https://doi.org/10.1145/2976022.2976030
• Search.GCL

  The content of this module is based on the paper Applications of Applicative Proof Search by Liam O'Connor https://doi.org/10.1145/2976022.2976030
• Search.Tychonoff.PartI

  This module is based on Todd Waugh Ambridge's blog post series "Search over uniformly continuous decidable predicates on infinite collections of types" https://www.cs.bham.ac.uk/~txw467/tychonoff/