<div dir="ltr">Hi All,<div><br></div><div>Can any one elaborate the Type Checking(and inference ) Algorithm used by Agda, provide or some pointers for the same. I am interested in the Type Checking of dependent types and since Agda has full support of &quot;dependent types&quot;, i assume It will be helpful looking at that. </div><div>Moreover , since the Typability of dependent type theory is undecidable in general( correct me if i am wrong here ), what approximations Agda uses to get a decidable type checker.</div><div><br></div><div>Thanks </div><div><br></div><div><br clear="all"><div><br></div>-- <br><div class="gmail_signature">Regards,<br>Ashish Mishra<br>Graduate Student,<br>Computer Science and Automation Department,IISc<br>Cell : +91-9611194714<br>Mailto : <a href="mailto:ashishmishra@csa.iisc.ernet.in" target="_blank">ashishmishra@csa.iisc.ernet.in</a><br><br></div>
</div></div>