[Agda] Type Checking in Agda

[Gabriel Scherer]

To complement these excellent recommendations with citations on the
inference/unification side:

- Higher-Order Dynamic Pattern Unification for Dependent Types and Records
  Andreas Abel and Brigitte Pientka (2011)
  http://www2.tcs.ifi.lmu.de/~abel/unif-sigma-long.pdf

- A tutorial implementation of dynamic pattern unification
  Adam Gundry and Conor McBride (2012)
  http://adam.gundry.co.uk/pub/pattern-unify/
  (this links give you the choice to read a more detailed chapter of
Adam Gundry's thesis instead)

- A Unification Algorithm for Coq Featuring Universe Polymorphism and
Overloading
  Beta Ziliani, Matthieu Sozeau (2015)
  https://www.mpi-sws.org/~beta/papers/unicoq.pdf

On Tue, Oct 27, 2015 at 7:39 AM, effectfully <effectfully at gmail.com> wrote:
>> Can any one elaborate the Type Checking(and inference ) Algorithm used by Agda, provide or some pointers for the same.
>
> Agda is far too complex language, there can't be a single exhaustive
> paper. Check these papers/posts first before you dive into
> metavariables resolution, irrelevance, coinduction, sized typed,
> instance arguments and whatever I forgot :
>
> http://augustss.blogspot.dk/2007/10/simpler-easier-in-recent-paper-simply.html
> http://www.andres-loeh.de/LambdaPi/LambdaPi.pdf
> http://math.andrej.com/2012/11/08/how-to-implement-dependent-type-theory-i/
> (and the other parts)
> https://github.com/sweirich/pi-forall
> http://www.andres-loeh.de/PiSigma/PiSigma.pdf
>
>> what approximations Agda uses to get a decidable type checker.
> Type checking is decidable in intensional type theories, which Agda
> is. It's type inference is undecidable.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda