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
• 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
• 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
• 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
• 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
• 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/