Publications
90 results found
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)
Van Bakel S, Lescanne P, 2008, Computation with classical sequents, 3rd International Workshop on Rewriting Calculus, Pages: 555-609
X is an untyped continuation-style formal language with a typed subset that provides a Curry-Howard isomorphism for a sequent calculus for implicative classical logic. X can also be viewed as a language for describing nets by composition of basic components connected by wires. These features make X an expressive platform on which many different (applicative) programming paradigms can be mapped. In this paper we will present the syntax and reduction rules for X; in order to demonstrate its expressive power, we will show how elaborate calculi can be embedded, such as the lambda-calculus, Bloo and Rose's calculus of explicit substitutions lambda x, Parigot's lambda mu and Curien and Herbelin's lambda mu mu.X was first presented in Lengrand (2003), where it was called the lambda xi-calculus. It can be seen as the pure untyped computational content of the reduction system for the implicative classical sequent calculus of Urban (2000).
van Bakel S, 2008, The heart of intersection type assignment: Normalisation proofs revisited, THEORETICAL COMPUTER SCIENCE, Vol: 398, Pages: 82-94, ISSN: 0304-3975
- Author Web Link
- Cite
- Citations: 6
van Bakel S, Berardi S, 2008, Classical Logic and Computation (2006) - Preface, ANNALS OF PURE AND APPLIED LOGIC, Vol: 153, Pages: 1-2, ISSN: 0168-0072
van Bakel S, De'Liguoro U, 2008, Logical equivalence for subtyping object and recursive types, 9th Italian Conference on Theoretical Computer Science (ICTCS 2005), Pages: 306-348
Subtyping in first order object calculi is studied with respect to the logical semantics obtained by identifying terms that satisfy the same set of predicates, as formalised through an assignment system. It is shown that equality in the full first order zeta-calculus is modelled by this notion, which in turn is included in a Morris-style contextual equivalence.
van Bakel S, Vigliotti MG, Kahn I, et al., 2008, Modelling intracellular fate of FGF receptors with BioAmbients, QAPL'08
van Bakel S, 2008, Reduction in Χ does not agree with Intersection and Union Types, International Workshop on Intersection Types and Related Systems (ITRS'08)
van Bakel S, Kahn I, Vigliotti MG, et al., 2008, Modelling intracellular fate of FGF receptors with BioAmbients, Electronic Notes in Computer Science, Vol: 220, Pages: 181-197
In this paper we consider a model of different sorting of receptors for Fibroblast Growth Factor via the endocytotic pathway. In order to accurately model the relocation in the different compartments of the cell by the ligand-receptor complex, we use the Stochastic version of Bioambients. The stochastic simulation is carried out using BAM (BioAmbient Abstract Machine), which is a Java implementation of BioAmbients via Gellispie's Algorithm. Our model and the associated results of the simulation shed light on different mechanisms that influence the spatial distribution of the different components in the pathway.
Steffen van Bakel, Ugo de'Liguoro, 2008, Logical equivalence for subtyping object and recursive types, Theory of Computing Systems
van Bakel S, Khan I, Vigliotti MG, et al., 2008, Modelling Intracellular Fate of FGF Receptors With BioAmbients., Pages: 181-197
van Bakel S, 2008, Subject Reduction vs Intersection / Union Types for lambda-bar-mu-mu-tilde, Visions of Computer Science, BCS's international academic conference, Publisher: British Computing Society
van Bakel S, 2008, Subject Reduction vs Intersection / Union Types for lambda-bar-mu-mu-tilde, Visions of Computer Science, Publisher: British Computer Society, Pages: 249-258
van Bakel S, 2008, The Heart of Intersection Type Assignment, Theoretical computer science, Vol: 398, Pages: 82-94
van Bakel S, Lescanne P, 2008, Computation with Classical Sequents, Mathematical Structures in Computer Science, Pages: 555-609
X is an untyped language for describing circuits by composition of basic components. This language is well suited to describe structures which we call ``circuits'' and which are made of parts that are connected by wires. Moreover X gives an expressive platform on which algebraic objects and many different (applicative) programming paradigms can be mapped. In this paper we will present the syntax and reduction rules for X and some its potential uses. To demonstrate the expressive power of X, we will show how, even in an untyped setting, elaborate calculi can be embedded, like the naturals, the lambda-calculus, Bloe and Rose's calculus of explicit substitutions lambda-x, Parigot's lambda-mu and Curien and Herbelin's lambda-mu-mu-tilde.
van Bakel S, Vigliotti MG, 2007, Note on a simple type system for non-interference, Nordic Workshop on Programming Theory (NWPT'07)
van Bakel S, Vigliotti MG, 2007, Note on a simple type system for non-interference, Nordic Workshop on Programming Theory (NWPT'07)
Kalliadasis S, Thiele U, 2007, Preface, CISM International Centre for Mechanical Sciences, Courses and Lectures, Vol: 490, ISSN: 0254-1971
van Bakel S, Vigliotti MG, 2007, Note on a simple type system for non-interference, Nordic Workshop on Programming Theory (NWPT'07)
Raghunandan J, van Bakel S, 2006, Explicit Alpha Conversion and Garbage Collection for X
Summer A, van Bakel S, 2006, Approaches to Polymorphism in Classical Sequent Calculus, 15th European Symposium on Programming (ESOP'06), Publisher: Springer-Verlag, Pages: 84-99
van Bakel S, Lengrand S, Lescanne P, 2005, The language X: Circuits, computations and classical logic, Berlin, 9th Italian Conference on Theoretical Computer Science (ICTCS 2005), 12 - 14 October 2005, Siena, ITALY, Publisher: Springer-Verlag, Pages: 81-96
van Bakel S, de'Liguoro U, 2005, Subtyping object and recursive types logically, Tenth Italian Conference on Theoretical Computer Science (ICTCS'05), Publisher: Springer, Pages: 66-80
van Bakel S, de'Liguoro U, 2005, Subtyping object and recursive types logically (Extended abstract), 9th Italian Conference on Theoretical Computer Science (ICTCS 2005), Publisher: SPRINGER-VERLAG BERLIN, Pages: 66-80, ISSN: 0302-9743
- Author Web Link
- Cite
- Citations: 3
van Bakel S, Lengrand S, Lescanne P, 2005, The language <i>X</i>:: Circuits, computations and classical logic (Extended abstract), 9th Italian Conference on Theoretical Computer Science (ICTCS 2005), Publisher: SPRINGER-VERLAG BERLIN, Pages: 81-96, ISSN: 0302-9743
- Author Web Link
- Cite
- Citations: 12
van Bakel S, De Liguoro U, 2005, Subtyping object and recursive types logically, Berlin, 9th Italian Conference on Theoretical Computer Science (ICTCS 2005), 12 - 14 October 2005, Siena, ITALY, Publisher: Springer-Verlag, Pages: 66-80
Raghunandan J, van Bakel S, 2004, Implementing X, Electronic Notes in Theoretical Computer Science, Publisher: Elsevier Science Bv
Raghunandan J, van Bakel S, 2004, Implementing X, Electronic Notes in Theoretical Computer Science, Publisher: Elsevier Science Bv
Lengrand S, Lescanne P, Dougherty D, et al., 2004, Intersection types for explicit substitutions, INFORMATION AND COMPUTATION, Vol: 189, Pages: 17-42, ISSN: 0890-5401
- Author Web Link
- Cite
- Citations: 21
van Bakel S, 2004, Intersection and Union Types for X, International Workshop on Intersection Types and Related Systems (ITRS'04), Publisher: ENTCS
van Bakel S, 2004, Cut-elimination in the strict intersection type assignment system is strongly normalising, Notre Dame Journal of Formal Logic, Vol: 45, Pages: 35-125, ISSN: 0029-4527
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.