System ST

• Autorzy: Raffalli Ch.
• Języki publikacji: PL

Abstrakty

EN

This article is a set of commented slides presenting a new type system: "System ST" (ST stands for SubTyping), based on subtyping. The extraordinary expressive power of the system (not really visible in this set of slides) leads us to think that it could be a good candidate for doing both proofs and extractions of programs. The main argument to support this claim is the completeness of the system which says that if a program can be proved correct (using realizability), then it can be extracted from a proof.

• Wydawca: Wydawnictwo Uniwersytetu Jagiellońskiego
• Czasopismo: Schedae Informaticae
• Rocznik: 2003
• Tom: Vol. 12
• Strony: 97--111
• Opis fizyczny: Bibliogr. 28 poz.

Twórcy

autor

Raffalli Ch.

• Laboratoire de Mathematique, Universite de Savoie, 73376 Le Bourget-du-Lac cedex (France), LAMA, Savoie University,

Bibliografia

• [1] Aspinall D.; Subtyping with Singleton Types, in: Computer Science Logic, CSL’94, Lecture Notes in Computer Science, Springer-Verlag, Vol. 933, 1995, pp. 1-15.
• [2] Berardi S.; Pruning simply typed X-terms, Journal of Logic and Computation, Vol. 6, 1996, pp. 663-681.
• [3] Boerio L.; Optimizing Programs Extracted From Proofs, Ph.D. thesis, Computer Science Department of Torino University, 1995.
• [4] Church A.; A formulation of the simple theory of types, Journal of Symbolic Logic, Vol. 5, 1940, pp. 56-80.
• [5] Coquand T., Huet G.; The calculus of construction, in: Information and Com-putation, 1988, pp. 241-262.
• [6] Courant J.; Strong Normalization with Singleton Types, in: S. Van Bakel, (ed.), Second Workshop on Intersection Types and Related Systems, Lecture Notes in Computer Science, Copenhaguen, Danemark, July 2002, Elsevier, Vol. 70.
• [7] Curmin P.; Marquage des preuves et extraction de programmes. Ph.D. thesis, Equipe de logique Université Paris VII, 1999.
• [8] Girard J.-Y.; The system F of variable types: fifteen years later, Theoretical Computer Science, Vol. 45, 1986, pp. 159-192.
• [9] Harper R., Stone C.; Deciding Type Equivalence with Singleton Kinds, in: Symposium on Principles of Programming Languages, 2000, pp. 214-227.
• [10] Hoare C.A.R.; An axiomatic Basis For Computer Programming. Communication of the ACM, October 1969, Vol. 12(10), pp. 576-580.
• [11] Hofmann M., Pierce B.; Positive subtyping, Technical report, LFCS, 1994, report number 94-303.
• [12] Howard W.A.; The formulae-as-types notion of construction, to: H.B. Curry, Essays on combinatory logic, X-calculus and formalism, 1980, pp. 479-490.
• [13] Krivine J.-L.; Un algorithme non typable dans le système F, in: Comptes Rendus de l'Académie des Sciences de Paris, Vol. 304, Série I, 1987, pp. 123-126.
• [14] Krivine J.-L.; Lambda-Calculus: Types and Models. Computers and their applications, Ellis Horwood, 1993.
• [15] Krivine J.-L., Parigot M.; Programming with Proofs, Inf. Process. Cybern., EIK, Vol. 26(3), 1990, pp. 149-167.
• [16] Coppo M., Dezani-Ciancaglini M.; A New Type Assignment System for Lambda-Terms, Archives for Mathematical Logic, Vol. 19, 1978, pp. 139-156.
• [17] Mitchell J.C.; Polymorphic type inference and containment, Information and Computation, Vol. 76, 1988, pp. 211-249.
• [18] Parent C.; Synthesizing proofs from programs in the Calculus of Inductive Constructions, in: Mathematics for Programs Constructions, Lecture Notes in Computer Science, Springer-Verlag, Vol. 947, 1995.
• [19] Parigot M.; Programming with Proofs: a Second Order Type Theory, Lecture Notes in Computer Science, Vol. 300, 1988. Communication at ESOP.
• [20] Parigot M.; Recursive programming with proofs, Theoretical Computer Science, Vol. 94, 1992, pp. 335-356.
• [21] Paulin-Mohring C.; Extracting Fω’s programs from proofs in the Calculus of Constructions, in: Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, January 1989, ACM.
• [22] Paulin-Mohring C., Werner B.; Synthesis of ML programs in system Coq, Journal of Symbolic Logic, Vol. 15, 1993, pp. 607-640.
• [23] Pierce B.C.; Programming with Intersection Types, Union Types, and Polymorphism, Technical Report CMU-CS-91-106, CMU, 1991.
• [24] Pottier F.; Type inference in the presence of subtyping: from theory to practice, Technical report, INRIA, 1998. Report number: 3483.
• [25] Raffalli C.; System ST, ß-reduction and completeness, prepublication du LAMA numero 02-4d, to be presented at LICS 2003 and available from the web page of the author, 2001.
• [26] Raffalli C.; System ST, Toward A Type System for Extraction AND Proof of Programs, prepublication du LAMA numero 01-12c, to appear in APAL and available from the web page of the author, 2001.
• [27] Raffalli C.; The PhoX proof assistant version 0.8, software available on the Internet: http://wwwJama.univ-savoie.fr/~raffalli/phox.html, 2002.
• [28] Severi P., Szasz N.; Studies of a Theory of Specifications with built-in Program Extraction, Journal of Automated Reasoning, Vol. 27(1), July 2001.