![]() Reus, B.: Synthetic domain theory in type theory: Another logic of computable functions, in Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs'96, LNCS 1125, 1996, pp. Thesis, Ludwig-Maximilians-Universit ät M ünchen, 1995. Reus, B.: Program Verification in Synthetic Domain Theory, Ph.D. Prawitz, D.: Natural Deduction A Proof-Theoretical Study, Stockholm Studies in Philosophy 3, Almqvist and Wiksell, 1965. Smith (eds.), Twenty Five Years of Constructive Type Theory, Oxford Univ. Pollack, R.: How to believe a machine-checked proof, in G. Plotkin (eds.), Proceedings of the Second International Conference on Typed Lambda Calculi and Applications, TLCA'95, Edinburgh, 1995. Pollack, R.: A verified typechecker, in M. Pollack, R.: The Theory of LEGO: A Proof Checker for the Extended Calculus of Constructions, Ph.D. Nipkow (eds.), TYPES'93: Workshop on Types for Proofs and Programs, Nijmegen, May 1993, Selected Papers, LNCS 806, 1994, pp. Pollack, R.: Closure under alpha-conversion, in H. Plotkin, G.: Call-by-name, call-by-value, and the λ-calculus, Theoret. Pfenning, F.: A proof of the Church-Rosser theorem and its representation in a logical framework, Technical Report CMU-CS-92-186, Carnegie Mellon University, 1992. Nipkow, T.: More Church-Rosser proofs (in Isabelle/HOL), in Automated Deduction - CADE-13, LNCS 1104, 1996, pp. Mitschke, G.: The standardisation theorem for λ-calculus, Z. Groote (eds.) Proceedings of the International Conference on Typed Lambda Calculi and Applications, TLCA'93, Utrecht, 1993, pp. and Pollack, R.: Pure Type Systems formalized, in M. ![]() Paulin-Mohring (eds.), TYPES'96: Workshop on Types for Proofs and Programs, Aussois Selected Papers, 1998, to appear. McBride, C.: Inverting inductively defined relations in LEGO, in E. Martin-L öf, P.: A theory of types, Technical Report 71-3, University of Stockholm, 1971. and Pollack, R.: LEGO proof development system: User' manual, Technical Report ECS-LFCS-92-211, Computer Science Dept., Univ. Luo, Z.: Computation and Reasoning: A Type Theory for Computer Science, International Series of Monographs on Computer Science, Oxford University Press, 1994. Luo, Z.: Program specification and data refinement in type theory, in ' 91, Vol. Kleymann, T.: Hoare Logic and VDM: Machine-Checked Soundness and Completeness Proofs, Ph.D. C.: Introduction to Metamathematics, Nostrand, Princeton, 1952. and Pollack, R.: Incremental changes in LEGO: 1993. Huet, G.: Residual theory in λ-calculus: A formal development, J. Narasimhan (ed.), A Perspective in Theoretical Computer Science, World Scientific Publishing, 1989. and Melham, T.: Five axioms of alpha conversion, in Von Wright, Grundy, and Harrison (eds.), Ninth Conference on Theorem Proving in Higher Order Logics TPHOL'96, Turku, LNCS 1125, 1996, pp. and Nederhof, M.-J.: A modular proof of strong normalization for the calculus of constructions, J. Thesis, Department of Mathematics and Computer Science, University of Nijmegen, 1993. Geuvers, H.: Logics and Type Systems, Ph.D. Gentzen, G.: The Collected Papers of Gerhard Gentzen, Studies in Logic and the Foundations of Mathematics, North-Holland, 1969. Odifreddi (ed.), Logic and Computer Science, APIC Studies in Data Processing 31, Academic Press, 1990, pp. Gallier, J.: On Girard' “ Candidats de reductibilit é, in P. and Pitts, A.: A new approach to abstract syntax involving binders, in G. Geuvers (ed.), Informal Proceedings of the Nijmegen Workshop on Types for Proofs and Programs, 1993.įeferman, S.: Finitary inductively presented logics, in ' 88, Padova, North-Holland, 1988. and Boyer, R.: Towards checking proof checkers, in H. Plotkin (eds.), Logical Frameworks, 1991.Ĭoquand, T.: An algorithm for type-checking dependent types, Sci. Ĭoquand, T.: An algorithm for testing conversion in type theory, in G. ![]() Thesis, Dipartimento di Informatica, Torino, Italy, 1990.Ĭardelli, L.: F-sub, the system, Technical report, DEC Systems Research Centre, 1991.Ĭoquand, C.: Combinator shared reduction and infinite objects in type theory, 1996. 34-57.īerardi, S.: Type Dependence and Constructive Mathematics, Ph.D. P.-A.: On the subject reduction property for algebraic type systems, in CSL'96: Proceedings of the 10th Annual Conference of the European Association for Computer Science Logic, Utrecht, LNCS 1258, 1997, pp. et al.: The Coq proof assistant reference manual, INRIA-Rocquencourt, 1998.īarras, B.: Coq en Coq, Rapport de Recherche 3026, INRIA, 1996.īarthe, G. II, Oxford University Press, 1992.īarras, B. Altenkirch, T.: A formalization of the strong normalization proof for System F in LEGO, in Proceedings of the International Conference on Typed Lambda Calculi and Applications, TLCA'93, LNCS 664, 1993.īarendregt, H.: Lambda calculi with types, in Abramsky, Gabbai, and Maibaum (eds.), Handbook of Logic in Computer Science, Vol.
0 Comments
Leave a Reply. |