PL EN


Preferencje help
Widoczny [Schowaj] Abstrakt
Liczba wyników
Tytuł artykułu

A Behavioural Lambda Model

Wybrane pełne teksty z tego czasopisma
Identyfikatory
Warianty tytułu
Języki publikacji
PL
Abstrakty
EN
We build a lambda model which characterizes completely (persistently) normalizing, (persistently) head normalizing, and (persistently) weak head normalizing terms. This is proved by using the finitary logical description of the model obtained by defining a suitable intersection type assignment system.
Rocznik
Tom
Strony
35--47
Opis fizyczny
Bibliogliogr, 28 poz., rys.
Twórcy
  • Dipartimento di Informatica, Universita di torino, Torino, Italy
autor
  • Faculty of Engineering, University of Novi Sad, Novi Sad, Yugoslavia
Bibliografia
  • [1] Abramsky S.; Domain theory in logical form, Ann. Pure Appl. Logic, Vol. 51(1-2), 1991, pp. 1-77.
  • [2] Alessi F.; Strutture di tipi, teoria dei domini e modelli del lambda calcolo, Ph.D. thesis, Torino University, 1991.
  • [3] Amadio R.M., Curien P.L.; Domains and Lambda-Calculi. Cambridge University Press, Cambridge 1998.
  • [4] Barendregt H., Coppo M., Dezani-Ciancaglini M.; A filter lambda model and the completeness of type assignment, J. Symbolic Logic, Vol. 48(4), 1983, pp. 931-940.
  • [5] Barendregt H.P.; The Lambda Calculus: Its Syntax and Semantics, North- Holland, Amsterdam, revised edition, 1984.
  • [6] Böhm C., Dezani-Ciancaglini M.; A-terms as total or partial functions on normal forms, in: C. Böhm, (ed.). A-calculus and Computer Science Theory, Lecture Notes in Computer Science, Springer-Verlag, Vol. 37, Berlin 1975, pp. 96-121.
  • [7] Coppo M., Dezani-Ciancaglini M., Honsell F., Longo G.; Extended type structures and filter lambda models, in: G. Lolli, G. Longo, and A. Marcja, (eds.), Logic colloquium ’82, North-Holland, Amsterdam 1984, pp. 241-262.
  • [8] Dezani-Ciancaglini M., Ghilezan S.; A lambda model characterizing computational behaviours of terms, in: Y. Toyama, (ed.), International Workshop on Rewriting in Proof and Computation, RPC'01, 2001, pp. 100-119.
  • [9] Dezani-Ciancaglini M., Ghilezan S.; Two behavioural lambda models, in: H. Geuvers and F. Wiedijk, (eds.), TYPES 2002, Lecture Notes in Computer Science, Springer-Verlag, 2003 (to appear).
  • [10] Dezani-Ciancaglini M., Honsell F., Motohama Y.; Compositional characterization of X-terms using intersection types, in: M. Nielsen and B. Rovan, (eds.), Mathematical Foundations of Computer Science 2000, Lecture Notes in Computer Science, Springer-Verlag, Vol. 1893, 2000, pp. 304-313.
  • [11] Gallier J.; Typing untyped X-terms, or reducibility strikes again!, Ann. Pure Appl. Logic, Vol. 91, 1998, pp. 231-270.
  • [12] Ghilezan S.; Strong normalization and typability with intersection types, Notre Dame J. Formal Logic, Vol. 37(1) , 1996, pp. 44-52.
  • [13] Girard J.Y.; Une extension de l’interprétation de Gôdel à l’analyse, et son application à l’élimination des coupures dans l’analyse et la théorie des types, in: J.E. Fenstadt., (éd.), 2nd Scandinavian Logic Symposium, North-Holland, 1971, pp. 63-92.
  • [14] Johnstone P.T.; Stone Spaces, Cambridge University Press, Cambridge 1986, reprint of the 1982 edition.
  • [15] Kegelman M.; Continuous Domains in Logical Form, Ph.D. thesis, School of Computer Science, The University of Birmingham, 1999, http://www.cs.bham.ac.uk/âxj/former-students.html
  • [16] Krivine J.L.; Lambda-calcul Types et modèles, Masson, Paris 1990.
  • [17] Leivant, D.; Typing and computational properties of lambda expressions, Theoret. Comput. Sci., Vol. 44(1). 1986, pp. 51-68.
  • [18] Martin-Löf P.; Lecture notes on domain interpretation of type theory. Programming Methodology Group, Workshop on the Semantics of Programming Languages. Chalmers University of Technology, 1983.
  • [19] Mitchell J.C.; Type systems for programming languages, in: J. van Leeuvven, (ed.), Handbook of Theoretical Computer Science, Elsevier, Amsterdam. Vol. B, 1990, pp. 415-431.
  • [20] Mitchell J.C.; Foundation for Programmimg Languages, MIT Press, Boston 1996.
  • [21] Plotkin G.D.; Set-theoretical and other elementary models of the X-calculus, Theoret. Comput. Sei., Vol. 121(1-2), 1993, pp. 351-409.
  • [22] Pöttinger G.; A type assignment for the strongly normalizable X-terms, in: J.P. Seldin and J.R. Hindley, (eds.), To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press, London 1980, pp. 561-577.
  • [23] Scott D.S.; Continuous lattices, in: F.W. Lawvere, (ed.), Toposes, Algebraic Geometry and Loqic. Lecture Notes in Mathematics, Springer-Verlag, Vol. 274, Berlin 1972, pp. 97-136.
  • [24] Scott D.S.; Open problem, in: C. Böhm, (ed.). Lambda Calculus and Computer Science Theory, Lecture Notes in Computer Science, Springer-Verlag, Vol. 37, Berlin 1975, p. 369.
  • [25] Scott D.S.; Domains for denotational semantics, in: M. Nielsen and E.M. Schmidt, (eds.), Automata. Languages and Programming, Lecture Notes in Computer Science, Springer-Verlag, Vol. 140. Berlin 1982, pp. 577-613.
  • [26] Tait W.W.; Intensional interpretations of functionals of finite type I, Journal of Symbolic Logic, Vol. 32, 1967, pp. 198-212.
  • [27] Tait W.W.; .4 realizability interpretation of the theory of species, In R. Parikh, (ed.), Logic Colloquium, Lecture Notes in Mathematics, Springer-Verlag, Vol. 453, Berlin 1975, pp. 240-251.
  • [28] van Bakel S.: Complete restrictions of the intersection type discipline, Theoret. Comput. Sci., 1992, Vol. 102(1), pp. 135-163.
Typ dokumentu
Bibliografia
Identyfikator YADDA
bwmeta1.element.baztech-article-BUJ1-0016-0045
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.