Publications
90 results found
van Bakel S, 2019, Exception handling and classical logic, International Symposium on Principles and Practice of Programming Languages, Publisher: ACM
We present λtry, an extension of the λ-calculus with named exception handling, via try, throw and catch, and present a basic notion of type assignment expressing recoverable exception handling and show that it is sound. We define an interpretation for λtry to Parigot's λμ-calculus, and show that reduction (both lazy and call by value) is preserved by the interpretation. We will show that also types assignable in the basic system are preserved by the interpretation.We will then add a notion of total failure through halt that escapes applicative contexts without being caught by a handler, and show that we can interpret this in λμ when adding top as destination. We will argue that introducing handlers for halt will break the relation with λμ.We will conclude the paper by showing that it is possible to add handlers for program failure by introducing panic and dedicated handlers to λtry. We will need to extend the language with a conditional construct that is typed in a non-traditional way, that cannot be expressed in λμ or logic. This will allow both recoverable exceptions and total failure, dealt with by handlers; we will show a non-standard soundness result for this system.
van Bakel S, Barbanera F, de'Liguoro U, 2018, Orchestrated compliance for session-based client/server interactions, Electronic Proceedings in Theoretical Computer Science, EPTCS 189, ISSN: 2075-2180
van Bakel S, 2018, Characterisation of normalisation properties for λμ using Strict negated intersection types, ACM Transactions on Computational Logic, Vol: 19, Pages: 1-47, ISSN: 1529-3785
We show characterisation results for normalisation, head-normalisation, and strong normalisation for λ μ using intersection types. We reach these results for a strict notion of type assignment for λ μ that is the natural restriction of the domain-based system of van Bakel et al. (2011) for λ μ by limiting the type inclusion relation to just intersection elimination. We show that this system respects β μ-equality, by showing both soundness and completeness results. We then define a notion of reduction on derivations that corresponds to cut-elimination, and show that this is strongly normalisable.We use this strong normalisation result to show an approximation result, and through that a characterisation of head-normalisation. Using the approximation result, we show that there is a very strong relation between the system of van Bakel et al. (2011) and ours.We then introduce a notion of type assignment that eliminates ω as an assignable type, and show, using the strong normalisation result for derivation reduction, that all terms typeable in this system are strongly normalisable as well, and show that all strongly normalisable terms are typeable.We conclude by adding type variables to our system, and show that system essentially is that of van Bakel (2010b).
van Bakel S, Barbanera F, de'Liguoro U, 2018, Intersection types for the λμ-calculus, Logical Methods in Computer Science (LMCS), Vol: 14, ISSN: 1860-5974
We introduce an intersection type system for the lambda-mu calculus that is invariant under subject reduction and expansion. The system is obtained by describing Streicher and Reus's denotational model of continuations in the category of omega-algebraic lattices via Abramsky's domain-logic approach. This provides at the same time an interpretation of the type system and a proof of the completeness of the system with respect to the continuation models by means of a filter model construction. We then define a restriction of our system, such that a lambda-mu term is typeable if and only if it is strongly normalising. We also show that Parigot's typing of lambda-mu terms with classically valid propositional formulas can be translated into the restricted system, which then provides an alternative proof of strong normalisability for the typed lambda-mu calculus.
van Bakel S, 2017, Characterisation of approximation and (head) normalisation for λμ using strict intersection types, Eighth Workshopon Intersection Types and Related Systems (ITRS 2016), Pages: 20-30, ISSN: 2075-2180
We study the strict type assignment for λμ that is presented in [7]. We define a notion of approximants of λμ-terms, show that it generates a semantics, and that for each typeable term there is an approximant that has the same type. We show that this leads to a characterisation via assignable types for all terms that have a head normal form, and to one for all terms that have a normal form, as well as to one for all terms that are strongly normalisable.
Barbanera F, van Bakel S, de'Liguoro U, 2017, Orchestrated session compliance, Journal of Logical and Algebraic Methods in Programming, Vol: 86, Pages: 30-76, ISSN: 2352-2208
We investigate the notion of orchestrated compliance for client/server interactions in the context of session contracts. The orchestrators we study have unbounded buffering capabilities and, besides never sending messages which have not been received, are such that any message from the client is eventually delivered by the orchestrator to the server. Moreover, no infinite interaction can consist definitely of messages from the server which are kept by the orchestrator. The subcontract relation induced by this new notion of compliance is also investigated.
van Bakel S, 2016, Approximation and (Head) Normalisation for λμ using Strict Intersection Types, Electronic Proceedings in Theoretical Computer Science, EPTCS 242, ISSN: 2075-2180
Van Bakel S, Vigliotti MG, 2014, A fully-abstract semantics of λμ in the π-calculus, Fifth International Workshop on Classical Logic and Computation (CL&C 2014), Pages: 33-47, ISSN: 2075-2180
We study the λμ-calculus, extended with explicit substitution, and define a compositional outputbased interpretation into a variant of the π-calculus with pairing that preserves single-step explicit head reduction with respect to weak bisimilarity. We define four notions of weak equivalence for λμ-one based on weak reduction ∼<inf>wβμ</inf>, two modelling weak head-reduction and weak explicit head reduction, ∼<inf>wH</inf> and ∼<inf>wxH</inf> respectively (all considering terms without weak head-normal form equivalent as well), and one based on weak approximation ∼A-and show they all coincide. We will then show full abstraction results for our interpretation for the weak equivalences with respect to weak bisimilarity on processes.
Rowe RNS, van Bakel SJ, 2014, Semantic types and approximation for featherweight java, Theoretical Computer Science, Vol: 517, Pages: 34-74, ISSN: 0304-3975
We consider semantics for the class-based object-oriented calculus Featherweight Java (without casts) based upon approximation. We also define an intersection type assignment system for this calculus and show that it satisfies subject reduction and expansion, i.e. types are preserved under reduction and its converse. We establish a link between type assignment and the approximation semantics by showing an approximation result, which leads to a sufficient condition for the characterisation of head-normalisation and termination. We show the expressivity of both our calculus and our type system by defining an encoding of Combinatory Logic into our calculus and showing that this encoding preserves typeability. We also show that our system characterises the normalising and strongly normalising terms for this encoding. We thus demonstrate that the great analytic capabilities of intersection types can be applied to the context of class-based object orientation.
van Bakel S, Barbanera F, de'Liguoro U, 2013, Characterisation of Strongly Normalising lambda-mu-Terms, Electronic Proceedings in Theoretical Computer Science, Vol: 121, Pages: 1-17
van Bakel S, Berardi S, Berger U, 2013, Preface, Annals of Pure and Applied Logic, Vol: 164, Pages: 589-590, ISSN: 0168-0072
Bakel SV, Rowe RNS, 2013, Functional Type Assignment for Featherweight Java - To Rinus Plasmeijer, in Honour of His 61st Birthday., Publisher: Springer, Pages: 27-46
Bakel SV, Vigliotti MG, 2012, An Output-Based Semantics of Λμ with Explicit Substitution in the π-Calculus - Extended Abstract., Publisher: Springer, Pages: 372-387
van Bakel S, 2012, Completeness and Soundness results for X with Intersection and Union Types, Fundamenta Informaticae, Vol: 121, Pages: 1-41
van Bakel S, Barbanera F, de'Liguoro U, 2011, A Filter Model for the λμ-Calculus, Typed Lambda Calculi and Applications (TLCA'11), Publisher: Springer, Pages: 213-228
van Bakel S, Rowe R, 2011, Approximation Semantics and Expressive Predicate Assignment for Object-Oriented Programming, Typed Lambda Calculi and Applications (TLCA'11), Publisher: Springer-Verlag, Pages: 229-244
van Bakel S, 2011, Strict Intersection Types for the Lambda Calculus, ACM Computing Surveys, Vol: 43
van Bakel S, Berardi S, Berger U, 2011, Proceedings Third International Workshop on Classical Logic and Computation CL&C 2010, Third International Workshop on Classical Logic and Computation CL&C 2010
Bakel SV, Barbanera F, de'Liguoro U, 2011, A Filter Model for the λμ-Calculus - (Extended Abstract)., Publisher: Springer, Pages: 213-228
Bakel SV, 2011, Reduction in X does not agree with Intersection and Union Types (Extended abstract), CoRR, Vol: abs/1109.4570
van Bakel S, 2010, Completeness and partial soundness results for intersection and union typing for (λ)over-barμ(μ)over-tilde, ANNALS OF PURE AND APPLIED LOGIC, Vol: 161, Pages: 1400-1430, ISSN: 0168-0072
- Author Web Link
- Cite
- Citations: 8
van Bakel S, Berardi S, Berger U, 2010, Classical Logic and Computation (2008) Preface, ANNALS OF PURE AND APPLIED LOGIC, Vol: 161, Pages: 1313-1314, ISSN: 0168-0072
van Bakel S, 2010, Sound and Complete Typing for λμ, 5th International Workshop on Intersection Types and Related Systems (ITRS'10), Pages: 31-44
van Bakel S, 2010, Sound and Complete Typing for lambda mu, 5th International Workshop on Intersection Types and Related Systems (ITRS'10), Pages: 31-44
van Bakel S, Berardi S, Berger S, 2010, Proceedings Third International Workshop on Classical Logic and Computation CL&C 2010, Classical Logic and Computation CL&C 2010
van Bakel S, 2010, Strict Intersection Types for the Lambda Calculus, ACM Computing Surveys
van Bakel S, Vigliotti MG, 2009, A logical interpretation of the lambda-calculus into the pi-calculus, preserving spine reduction and types, 20th International Conference on Concurrency Theory (CONCUR'09), Publisher: Springer Verlag, Pages: 84-98, ISSN: 0302-9743
van Bakel S, Rowe R, 2009, Semantic Predicate Types and Approximation for Class-based Object Oriented Programming, 11th Workshop on Formal Techniques for Java-like Programs (FTfJP'09)
van Bakel S, 2008, The Heart of Intersection Type Assignment, Theoretical Computer Science
van Bakel S, Cardelli L, Vigliotti MG, 2008, From X to Pi: Representing Classical Sequent Calculus in Pi-calculus, International Workshop on Classical Logic and Computation (CL&C'08)
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.