References

1. T. Altenkirch, C. McBride & W. Swierstra (2007): Observational Equality, Now!. In: A. Stump & H. Xi: PLPV '07: Proceedings of the 2007 Workshop on Programming Languages meets Program Verification, pp. 57–68.
2. B. Barras & B. Bernardo (2008): The Implicit Calculus of Constructions as a Programming Language with Dependent Types. In: Roberto M. Amadio: Foundations of Software Science and Computational Structures, 11th International Conference, FOSSACS 2008, Lecture Notes in Computer Science 4962. Springer, pp. 365–379.
3. R. Constable & the PRL group (1986): Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall.
4. M. Coppo1 & M. Dezani-Ciancaglini (1978): A New Type Assignment for λ-terms. Archiv. Math. Logik 19(1), pp. 139–156.
5. R. Harper, F. Honsell & G. Plotkin (1993): A Framework for Defining Logics. Journal of the Association for Computing Machinery 40(1), pp. 143–184.
6. P. Martin-Löf (1984): Intuitionistic Type Theory. Bibliopolis.
7. C. McBride (1999): Dependently Typed Functional Programs and Their Proofs. Ph.D. thesis. University of Edinburgh.
8. A. Miquel (2001): The Implicit Calculus of Constructions. In: Typed Lambda Calculi and Applications, Lecture Notes in Computer Science 2044. Springer, pp. 344–359.
9. N. Mishra-Linger & T. Sheard (2008): Erasure and Polymorphism in Pure Type Systems. In: Roberto M. Amadio: Foundations of Software Science and Computational Structures, 11th International Conference (FOSSACS), Lecture Notes in Computer Science 4962. Springer, pp. 350–364.
10. A. Stump, M. Deters, A. Petcher, T. Schiller & T. Simpson (2009): Verified Programming in Guru. In: T. Altenkirch & T. Millstein: Programming Languges meets Program Verification (PLPV), pp. 49–58.

Comments and questions to: eptcs@eptcs.org

For website issues: webmaster@eptcs.org