A Logical Framework with Dependently Typed Records

• Autorzy: Coquand T. , Pollack R. , Takeyama M.
• Języki publikacji: EN
• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2005
• Tom: Vol. 65, nr 1,2
• Strony: 113--134
• Opis fizyczny: Bibliogr 29 poz.

Twórcy

autor

Coquand T.

• Chalmers Tekniska Högskola, Sweeden

autor

Pollack R.

• Edinburgh University, U.K.

autor

Takeyama M.

• National Institute of Advanced Industrial Science and Technology, Japan

Bibliografia

• [1] Allen, S.: A Non-Type-Theoretic Semantics For Type-Theoretic Language, Ph.D. Thesis, Cornell Univ., 1987, Report TR87-866.
• [2] Aspinall, D.: Subtyping with Singleton Types, Proc. Computer Science Logic, CSL’94, 933, 1995.
• [3] Augustsson, L.: Cayenne – a language with dependent types, ICFP ’98, 34(1), ACM, June 1999.
• [4] Barendregt, H. P.: The Lambda Calculus: Its Syntax and Semantics, vol. 103 of Studies in Logic and the Foundations of Mathematics, revised edition, North-Holland, 1984.
• [5] Betarte, G.: Dependent Record Types and Formal Abstract Reasoning, Ph.D. Thesis, Chalmers Univ. of Technology, 1998.
• [6] Betarte, G., Tasistro, A.: Extension of Martin-Löf’s Type Theory with Record Types and Subtyping, Twenty Five Years of Constructive Type Theory (G. Sambin, J. Smith, Eds.), Oxford Univ. Press, 1998.
• [7] Chrzaszcz: Modules in Coq Are and Will Be Correct, Types for Proofs and Programs, TYPES 2003, 3085, Springer-Verlag, 2004.
• [8] Coq: The Coq Project, 2002, http://coq.inria.fr/.
• [9] Coquand, T.: An Algorithm for Testing Conversion in Type Theory, Logical Frameworks (G. Huet, G. Plotkin, Eds.), Camb. Univ. Press, 1991.
• [10] Courant, J.: MC: A Module Calculus for Pure Type Systems, Technical Report 1217, CNRS Universitè Paris Sud 8623: LRI, June 1999.
• [11] Courant, J.: Strong Normalizationwith Singleton Types, Second Workshop on Intersection Types and Related Systems (S. V. Bakel, Ed.), 70, Elsevier, 2002.
• [12] Crary, K.: Sound and Complete Elimination of Singleton Kinds, Types in Compilation, TIC 2000, 2071, Springer-Verlag, 2000.
• [13] Girard, J.-Y.: Locus Solum: From the Rules of Logic to the Logic of Rules, Mathematical Structures in Computer Science, 11(3), 2001, 301–506.
• [14] Goguen, H.: A Syntactic Approach to Eta Equality in Type Theory, Proceedings of POPL 2005, 2005.
• [15] Harper, R., Lillibridge,M.: A type-theoretic approach to higher-order modules with sharing, POPL’94, ACM Press, 1994.
• [16] Harper, R., Pfenning, F.: On Equivalence and Canonical Forms in the LF Type Theory, ACM Trans. On Computational Logic, 200?, (To appear).
• [17] Hayashi, S.: Singleton, Union and Intersection Types for Program Extraction, Information and Computation, 109, 1994, 174–210.
• [18] Kopylov, A.: Dependent Intersection: A New Way of Defining Records in Type Theory, Proceedings of the eighteenth Annual IEEE Syposium on Logic in Computer Science (LICS-03), IEEE Computer Society, 2003.
• [19] Leroy, X.: Manifest types, modules, and separate compilation, POPL’94, ACM Press, 1994.
• [20] Leroy, X.: A syntactic theory of type generativity and sharing, Journal of Functional Programming, 6(5), September 1996, 667–698.
• [21] Luo, Z.: Computation and Reasoning: A Type Theory for Computer Science, International Series of Monographs on Computer Science, Oxford Univ. Press, 1994.
• [22] MacQueen, D.: Using Dependent Types to Express Modular Structure, POPL’86, 1986.
• [23] McKinna, J., Pollack, R.: Some Lambda Calculus and Type Theory Formalized, Journal of Automated Reasoning, 23(3–4), November 1999.
• [24] Miquel, A.: The Implicit Calculus of Constructions, 5th Conf. on Typed Lambda Calculi and Applications, TLCA’01 (S. Abramsky, Ed.), 2044, Springer-Verlag, 2001.
• [25] Nordström, B., Petersson, K., Smith, J.: Martin-Löf’s Type Theory, in: Handbook of Logic in Computer Science (Abramsky, Gabbai, Maibaum, Eds.), vol. 5, Oxford Univ. Press, 2001.
• [26] Pollack, et al.: The LEGO Proof Assistant, 2001, http://www.dcs.ed.ac.uk/home/lego/.
• [27] Pollack, R.: Dependently Typed Records in Type Theory, Formal Aspects of Computing, 13, 2002, 386–402.
• [28] Stone, C.: Singleton Kinds and Singleton Types, Ph.D. Thesis, Carnegie Mellon University, 2000, Report CMU-CS-00-153.
• [29] Stone, C., Harper, R.: Extensional Equivalence and Singleton Types, ACM Transactions on Computational Logic, 200?, To appear.