LINK [1] T. Altenkirch, N. A. Danielsson, A. Löh, and N. Oury, “PiSigma: Dependent Types without the Sugar,” In M. Blume, N. Kobayashi, and G. Vidal, editors, Functional and Logic Programming, 10th International Symposium, FLOPS 2010, Sendai, Japan, April 1921, 2010. Proceedings, pp.4055, 2010.
LINK [2] A. Bove and V. Capretta, “Modelling General Recursion in Type Theory,” Mathematical Structures in Computer Science, vol.15, no.4, pp.671708, 2005.
LINK [3] A. Bove, P. Dybjer, and U. Norell, “A brief overview of agdaA functional language with dependent types,” In S. Berghofer, T. Nipkow, C. Urban, and M. Wenzel, editors, TPHOLs, volume 5674 of Lecture Notes in Computer Science, pp.7378. Springer, 2009.
LINK [4] A. Bove, P. Dybjer, and A. SicardRamírez, “Embedding a logical theory of constructions in agda,” In T. Altenkirch and T. D. Millstein, editors, PLPV, pp.5966. ACM, 2009.
LINK [5] V. Capretta, “General recursion via coinductive types,” Logical Methods in Computer Science, vol.1, no.2, 2005.
LINK [6] A. Charguéraud, “Program verification through characteristic formulae,” In Proceedings of the 15th ACM SIGPLAN International Conference on Functional programming, ICFP'10, pp.321332, New York, NY, USA, ACM, 2010.
LINK [7] R. Constable and the PRL group. Implementing mathematics with the Nuprl proof development system. PrenticeHall, 1986.
LINK [8] J. Davis, M. Kaufmann, J S. Moore, and S. Swords, “ACL2 Solution to VSTTE 2012 Problem 2,” Website: http://www.cs.utexas.edu/users/moore/acl2/vstte2012/acl2dkms/problem2/
LINK [9] S. Feferman, In the Light of Logic. Oxford University Press, 1998.
LINK [10] R. Harper, F. Honsell, and G. Plotkin, “A framework for defining logics,” Journal of the Association for Computing Machinery, vol.40, no.1, pp.143184, Jan. 1993.
LINK [11] M. Hasegawa and Y. Kakutani, “Axioms for recursion in callbyvalue,” Higher Order Symbol. Comput., vol.15, no.23, pp.235264, Sept. 2002.
LINK [12] C. K. Hur, 2010. Message on the Agda mailing list: https://lists.chalmers.se/pipermail/agda/2010/001526.html
LINK [13] M. Kaufmann, P. Manolios, and J S. Moore, Computeraided Reasoning: An Approach. Springer Netherlands, 2000.
LINK [14] G. Kimmell, A. Stump, H. D. Eades III, P. Fu, T. Sheard, S. Weirich, C. Casinghino, V. Sjöberg, N. Collins, and K. Y. Ahn, “Equational reasoning about programs with general recursion and callbyvalue semantics,” In K. Claessen and N. Swamy, editors, PLPV, pp.1526. ACM, 2012.
LINK [15] A. Krauss, “Partial and nested recursive function definitions in higherorder logic,” Journal of Automated Reasoning, vol.44, no.4, pp.303336, 2010.
LINK [16] A. Krauss, “Recursive definitions of monadic functions,” In A. Bove, E. Komendantskaya, and M. Niqui, editors, Workshop on Partiality and Recursion in Interactive Theorem Provers (PAR), vol.43 of EPTCS, pp.113, 2010.
LINK [17] N. Linger, Irrelevance, Polymorphism, and Erasure in Type Theory. PhD thesis, Portland State University, 2008.
LINK [18] J. Longley and R. Pollack, “Reasoning about CBV functional programs in isabelle/HOL,” In K. Slind, A. Bunker, and G. Gopalakrishnan, editors, TPHOLs, vol.3223 of Lecture Notes in Computer Science, pp.201216, Springer, 2004.
LINK [19] M. Kaufmann and J S. Moore, A Precise Description of the ACL2 Logic, 1998. Available from the ACL2 web site.
LINK [20] R. Milner, “LCF: A way of doing proofs with a machine,” In J. Becvr, editor, Mathematical Foundations of Computer Science 1979, vol.74 of Lecture Notes in Computer Science, pp.146159. Springer Berlin/Heidelberg, 1979.
LINK [21] N. MishraLinger and T. Sheard, “Erasure and polymorphism in pure type systems,” In R. M. Amadio, editor, FoSSaCS, vol.4962 of Lecture Notes in Computer Science, pp.350364, Springer, 2008
LINK [22] A. Nanevski, G. Morrisett, and L. Birkedal, “Polymorphism and Separation in Hoare Type Theory,” In Proceedings of the eleventh ACM SIGPLAN International Conference on Functional Programming, pp.6273, ACM, 2006.
LINK [23] A. Nanevski, G. Morrisett, A. Shinnar, P. Govereau, and L. Birkedal, “Ynot: Dependent types for imperative programs,” In J. Hook and P. Thiemann, editors, Proceeding of the 13th ACM SIGPLAN international conference on Functional programming (ICFP), pp.229240, 2008.
LINK [24] T. Nipkow, L. C. Paulson, and M. Wenzel, Isabelle/HOL — A Proof Assistant for HigherOrder Logic, vol.2283 of LNCS. Springer, 2002.
LINK [25] N. Oury, 2008, Message on the coqclub mailing list: https://sympa.inria.fr/sympa/arc/coqclub/200806/msg00022.html
LINK [26] S. Owre, J. Rushby, and N. Shankar, “PVS: A prototype verification system,” In D. Kapur, editor, 11th International Conference on Automated Deduction (CADE), vol.607 of Lecture Notes in Artificial Intelligence, pp.748752, SpringerVerlag, Saratoga, NY, jun 1992.
LINK [27] S. Owre and N. Shankar, “PVS Solution to VSTTE 2012 Problem 2,” Website. http://www.csl.sri.com/users/shankar/pvsexamples/srivstte12competition.tgz
LINK [28] F. Pfenning and C. Schürmann, “System description: Twelf — A metalogical framework for deductive systems,” In 16th International Conference on Automated Deduction, 1999.
LINK [29] B. Pientka and J. Dunfield, “Beluga: A framework for programming and reasoning with deductive systems (system description),” In J. Giesl and R. Hähnle, editors, Automated Reasoning, 5th International Joint Conference, IJCAR 2010, Edinburgh, UK, July 1619, 2010. Proceedings, pp.1521, 2010.
LINK [30] A. Poswolsky and C. Schürmann, “System description: Delphin—A functional programming language for deductive systems,” Electr. Notes Theor. Comput. Sci., vol.228, pp.113120, 2009.
LINK [31] A. Simpson and G. Plotkin, “Complete axioms for categorical fixedpoint operators,” In Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science (LICS), pp.3041, IEEE Computer Society, 2000.
LINK [32] A. Stump and E. Austin, “Resource typing in guru,” In J.C. Filliâtre and C. Flanagan, editors, Proceedings of the 4th ACM Workshop Programming Languages meets Program Verification, PLPV 2010, Madrid, Spain, January 19, 2010, pp.2738, ACM, 2010.
LINK [33] A. Stump, M. Deters, A. Petcher, T. Schiller, and T. Simpson, “Verified programming in guru,” In T. Altenkirch and T. Millstein, editors, Programming Languges meets Program Verification (PLPV), 2009.
LINK [34] The Coq Development Team. The Coq Proof Assistant Reference Manual, Version 8.3. INRIA, 2010. Available from http://coq.inria.fr/V8.3/refman/
LINK [35] C. Walther and S. Schweitzer, “Automated termination analysis for incompletely defined programs,” In F. Baader and A. Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, 11th International Conference (LPAR), Montevideo, Uruguay, pp.332346, 2005.
LINK [36] A. K. Wright and M. Felleisen, “A syntactic approach to type soundness,” Info. Comput., vol.115, no.1, pp.3894, 1994.
