Publications
90 results found
de'Liguoro U, van Bakel S, 2003, Logical Semantics for the First Order Sigma Calculus, Lecture Notes in Computer Science, Pages: 202-215
van Bakel S, 2003, Rank 2 Types for Term Graph Rewriting, Electronic Notes in Theoretical Computer Science, Vol: 75, Pages: 1-20, ISSN: 1571-0661
van Bakel S, Fernández M, 2003, Normalization, approximation, and semantics for combinator systems, THEORETICAL COMPUTER SCIENCE, Vol: 290, Pages: 975-1019, ISSN: 0304-3975
- Author Web Link
- Cite
- Citations: 6
van Bakel S, de'Liguoro U, 2003, Logical semantics for the first order Varsigma Calculus, LECT NOTES COMPUT SC, Vol: 2841, Pages: 202-215, ISSN: 0302-9743
We investigate logical semantics of the first order zeta-calculus. An assignment system of predicates to first order typed terms of the OB1 calculus is introduced. We define retraction models for that calculus and an interpretation of terms, types and predicates into such models. The assignment system is then proved to be sound and complete w.r.t. retraction models.
van Bakel S, de'Liguoro U, 2003, Logical Semantics for the First Order Sigma Calculus, Berlin, Eighth Italian Conference on Theoretical Computer Science (ICTCS'03), Publisher: Springer, Pages: 202-215
van Bakel S, 2002, Strongly Normalising Cut-Elimination with Strict Intersection Types
van Bakel S, Dezani-Ciancaglini M, 2002, Characterising Strong Normalisation for Explicit Substitutions., LATIN'02, Pages: 356-370
We characterise the strongly normalising terms of a composition-free calculus of explicit substititions (with or without garbage collection) by means of an intersection type assignment system. The main novelty is a new cut-rule which allows to forget the context of the minor premise when the context of the main premise does not have an assumption for the cut variable.
van Bakel S, Barbanera F, Dezani-Ciancaglini M, et al., 2002, Intersection types for λ-trees, THEORETICAL COMPUTER SCIENCE, Vol: 272, Pages: 3-40, ISSN: 0304-3975
- Author Web Link
- Cite
- Citations: 4
Braghin C, Cortesi A, Focardi R, et al., 2002, Boundary inference for enforcing security policies in mobile ambients, Proceedings of 2nd IFIP international conference on theoretical computer science (TCS'02), Montreal, Canada, 2002, Publisher: Kluwer, Pages: 383-395
van Bakel S, 2002, Rank 2 Type Assignment for Applicative Term Graph Rewriting, Electronic Notes in Theoretical Computer Science, Vol: 75, Pages: 1-20, ISSN: 1571-0661
van Bakel S, 2002, Strongly normalising cut-elimination with strict intersection types, Electronic Notes in Theoretical Computer Science, Vol: 70, Pages: 1-18, ISSN: 1571-0661
van Bakel S, Barbanera F, Fernandez M, 2001, Polymorphic intersection type assignment for rewrite systems with abstraction and -rul, Departmental Technical Report: 01/1, Publisher: Department of Computing, Imperial College London, 01/1
We define two type assignment systems for first-order rewriting extended with application, -abstraction,and -reduction, using a combination of intersection types and second-order polymorphic types. The first systemis the general one, for which we prove subject reduction, and strong normalisation of typeable terms. The secondis a decidable subsystem of the first, by restricting to rank 2 (intersection and quantified) types. For this systemwe define, using an extended notion of unification, a notion of principal typing which is more general than ML’sprincipal type property, since also the types for the free variables of terms are inferred
van Bakel S, Fernndez M, 2000, Normalisation, approximation and semantics for typeable combinator systems, Departmental Technical Report: 2000/10, Publisher: Department of Computing, Imperial College London, 10
This paper studies normalization of typeable terms and the relation between approximation semantics and filter models for Combinator Systems. It presents notions of approximants for terms, intersection type assignment, and reduction on type derivations; the last will be proved to be strongly normalizable. With this result, it is shown that, for every typeable term, there exists an approximant with the same type, and a characterization of the normalization behaviour of terms using their assignable types is given. Then the two semantics are defined and compared, and it is shown that the approximants semantics is fully abstract but the filter semantics is not.
van Bakel S, Barbanera F, Fernandez M, 2000, Polymorphic Intersection Type Assignment for Rewrite Systems with Abstraction and beta-rule, Types for Proofs and Programs. International Workshop (TYPES'99), Publisher: Springer Verlag, Pages: 41-60
van Bakel S, Barbanera F, Fernandez M, 2000, Polymorphic intersection type assignment for rewrite systems with abstraction and beta-rule, Publisher: Springer Verlag
van Bakel S, Fernandez M, 1997, Normalization Results for Typeable Rewrite Systems, Information and Computation, Vol: 133, Pages: 73-116
van Bakel S, Liquori L, Ronchi della Rocca S, et al., 1997, Comparing Cubes of Typed and Type Assignment Systems, Annals of Pure and Applied Logic, Vol: 86, Pages: 267-303
van Bakel S, 1996, Rank 2 Intersection Type Assignment in Term Rewriting Systems, Fundamenta Informaticae, Vol: 26, Pages: 141-166
van Bakel S, Barbanera F, Fernandez M, 1996, Rewrite Systems with Abstraction and beta-rule: Types, Approximants and Normalization, 6th European Symposium on Programming (ESOP'96)., Publisher: Springer-Verlag, Pages: 387-403
van Bakel S, Fernandez M, 1996, Approximation and Normalization Results for Typeable Term Rewriting Systems, Second International Workshop on Higher Order Algebra, Logic and Term Rewriting (HOA '95), Publisher: Springer-Verlag, Pages: 17-36
van Bakel S, 1995, Intersection Type Assignment Systems, Theoretical Computer Science, Vol: 151, Pages: 385-435
van Bakel S, Fernandez M, 1995, (Head-)Normalization of Typeable Rewrite Systems, 6th International Conference on Rewriting Techniques and Applications (RTA'95), Pages: 279-293
van Bakel S, Fernandez M, 1994, Strong Normalization of Typeable Rewrite Systems, First International Workshop on Higher Order Algebra, Logic and Term Rewriting (HOA'93), Publisher: Springer Verlag, Pages: 20-39
van Bakel S, Liquori L, Ronchi della Rocca S, et al., 1994, Comparing Cubes, Third International Symposium on Logical Foundations of Computer Science (LFCS'94), Publisher: Springer Verlag, Pages: 353-365
van Bakel S, 1993, Essential Intersection Type Assignment, 13th Conference on Foundations of Software Technology and Theoretical Computer Science (FST&TCS'93), Pages: 13-23
van Bakel S, 1993, Partial Intersection Type Assignment in Applicative Term Rewriting Systems, International Conference on Typed Lambda Calculi and Applications (TLCA'93), Pages: 29-44
van Bakel S, 1993, Principal type schemes for the Strict Type Assignment System, Journal of Logic and Computation, Vol: 3, Pages: 643-670
van Bakel S, Smetsers S, Brock S, 1992, Partial Type Assignment in Left Linear Applicative Term Rewriting Systems, 17th Colloquim on Trees in Algebra and Programming (CAAP'92), Publisher: Springer-Verlag, Pages: 300-321
van Bakel S, 1992, Complete restrictions of the Intersection Type Discipline, Theoretical Computer Science, Vol: 102, Pages: 135-163
van Bakel S, Barbanera F, Fernandez M, Polymorphic Intersection Type Assignment for Rewrite Systems with Abstraction and beta-rule, Types for Proofs and Programs. International Workshop, TYPES'99, Pages: 41-60
This data is extracted from the Web of Science and reproduced under a licence from Thomson Reuters. You may not copy or re-distribute this data in whole or in part without the written consent of the Science business of Thomson Reuters.