Communication publiée dans un ouvrage (Colloques, congrès, conférences scientifiques et actes)
Towards a Formally Verified Proof Assistant
Anand, Abhishek; RAHLI, Vincent
2014 • In Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings
Anand, Abhishek; Cornell University > Computer Science Department
RAHLI, Vincent ; Cornell University > Computer Science Department
Co-auteurs externes :
yes
Langue du document :
Anglais
Titre :
Towards a Formally Verified Proof Assistant
Date de publication/diffusion :
2014
Nom de la manifestation :
ITP 2014
Date de la manifestation :
July 2014
Titre de l'ouvrage principal :
Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings
Abbott, M., Altenkirch, T., Ghani, N.: Representing nested inductive types using W-types. In: Díaz, J., Karhumäki, J., Lepistö, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 59-71. Springer, Heidelberg (2004)
Allen, S.F.: A Non-Type-Theoretic Semantics for Type-Theoretic Language. PhD thesis, Cornell University (1987)
Allen, S.F., Bickford, M., Constable, R.L., Eaton, R., Kreitz, C., Lorigo, L., Moran, E.: Innovations in computational type theory using Nuprl. J. Applied Logic 4(4), 428-469 (2006), http://www.nuprl.org/
Anand, A., Rahli, V.: Towards a formally verified proof assistant. Technical report, Cornell University (2014), http://www.nuprl.org/html/ Nuprl2Coq/
Aydemir, B.E., Charguéraud, A., Pierce, B.C., Pollack, R., Weirich, S.: Engineering formal metatheory. In: POPL 2008, pp. 3-15. ACM (2008)
Barras, B.: Sets in Coq, Coq in sets. Journal of Formalized Reasoning 3(1), 29-48 (2010)
Bertot, Y., Casteran, P.: Interactive Theorem Proving and Program Development. Springer (2004), http://coq.inria.fr/
Bove, A., Dybjer, P., Norell, U.: A brief overview of Agda - A functional language with dependent types. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 73-78. Springer, Heidelberg (2009), http://wiki.portal.chalmers.se/agda/pmwiki.php
Brady, E.: Idris -: systems programming meets full dependent types. In: 5th ACM Workshop Programming Languages meets Program Verification, PLPV 2011, pp. 43-54. ACM (2011)
Buisse, A., Dybjer, P.: Towards formalizing categorical models of type theory in type theory. Electr. Notes Theor. Comput. Sci. 196, 137-151 (2008)
Capretta, V.: A polymorphic representation of induction-recursion (2004), http://www.cs.ru.nl/~venanzio/publications/induction-recursion.ps
Constable, R.L., Allen, S.F., Bromley, H.M., Cleaveland, W.R., Cremer, J.F., Harper, R.W., Howe, D.J., Knoblock, T.B., Mendler, N.P., Panangaden, P., Sasaki, J.T., Smith, S.F.: Implementing mathematics with the Nuprl proof development system. Prentice-Hall, Inc., Upper Saddle River (1986)
Crary, K.: Type-Theoretic Methodology for Practical Programming Languages. PhD thesis, Cornell University, Ithaca, NY (August 1998)
Danielsson, N.A.: A formalisation of a dependently typed language as an inductive-recursive family. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol. 4502, pp. 93-109. Springer, Heidelberg (2007)
Dybjer, P.: A general formulation of simultaneous inductive-recursive definitions in type theory. J. Symb. Log. 65(2), 525-549 (2000)
Dybjer, P., Setzer, A.: Induction-recursion and initial algebras. Ann. Pure Appl. Logic 124(1-3), 1-47 (2003)
Gonthier, G., Asperti, A., Avigad, J., Bertot, Y., Cohen, C., Garillot, F., Le Roux, S., Mahboubi, A., O'Connor, R., Biha, S.O., Pasca, I., Rideau, L., Solovyev, A., Tassi, E., Théry, L.: A machine-checked proof of the odd order theorem. In: ITP 2013, [1], pp. 163-179
Harrison, J.: Towards Self-verification of HOL Light. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 177-191. Springer, Heidelberg (2006)
Howe, D.J.: Equality in lazy computation systems. In: Proceedings of Fourth IEEE Symposium on Logic in Computer Science, pp. 198-203. IEEE Computer Society (1989)
Howe, D.J.: Semantic foundations for embedding HOL in Nuprl. In: Wirsing, M., Nivat, M. (eds.) AMAST 1996. LNCS, vol. 1101, pp. 85-101. Springer, Heidelberg (1996)
Hur, C.-K., Neis, G., Dreyer, D., Vafeiadis, V.: The power of parameterization in coinductive proof. In: POPL 2013, pp. 193-206. ACM (2013)
Kopylov, A.: Type Theoretical Foundations for Data Structures, Classes, and Objects. PhD thesis, Cornell University, Ithaca, NY (2004)
Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. In: POPL 2014, pp. 179-192. ACM (2014)
Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: POPL 2006, pp. 42-54. ACM (2006)
McBride, C.: Hier soir, an OTT hierarchy (2011), http://sneezy.cs.nott. ac.uk/epilogue/?p=1098
Mendler, P.F.: Inductive Definition in Type Theory. PhD thesis, Cornell University, Ithaca, NY (1988)
Myreen, M.O., Davis, J.: A verified runtime for a verified theorem prover. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 265-280. Springer, Heidelberg (2011)
Myreen, M.O., Davis, J.: The reflective milawa theorem prover is sound (Down to the machine code that runs it). In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS (LNAI), vol. 8558, pp. 413-428. Springer, Heidelberg (2014)
Myreen, M.O., Owens, S., Kumar, R.: Steps towards verified implementations of hol light. In: ITP 2013 [1], pp. 490-495
Paulin-Mohring, C.: Inductive definitions in the system Coq - rules and properties. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664, pp. 328-345. Springer, Heidelberg (1993)
Rahli, V., Bickford, M., Anand, A.: Formal program optimization in Nuprl using computational equivalence and partial types. In: ITP 2013, [1], pp. 261-278
Setzer, A.: Proof theoretical strength of Martin-Löf Type Theory with W-type and one universe. PhD thesis, Ludwig Maximilian University of Munich (1993)
I.A.S. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Univalent Foundations (2013)
Werner, B.: Sets in types, types in sets. In: Ito, T., Abadi, M. (eds.) TACS 1997. LNCS, vol. 1281, pp. 530-546. Springer, Heidelberg (1997)
