7 citations · 11 across the 5 of their papers we have counts for
5 papers · 1 filter
Comparing Call-by-Name and Call-by-Value Reduction and Reduction Strategies in Calculi for Classical Logic
Steffen van Bakel, David Davies
We define call-by-name and call-by-value reduction and reduction strategies for the calculi slmu (symmetric lmu), lmmt, and Xs (X with implicit substitution). We establish a strong…
Characterisation of Approximation and (Head) Normalisation for using Strict Intersection Types
Steffen van Bakel
We study the strict type assignment for lambda-mu that is presented in [van Bakel'16]. We define a notion of approximants of lambda-mu-terms, show that it generates a semantics, an…
Proceedings Sixth International Workshop on Classical Logic and Computation
Ulrich Kohlenbach, Steffen van Bakel, Stefano Berardi
The workshop series intends to cover research that investigates the computational aspects of classical logic and mathematics. Its focus is on unwinding the computational content of…
Proceedings Third International Workshop on Classical Logic and Computation
Steffen van Bakel, Stefano Berardi, Ulrich Berger
The fact that classical mathematical proofs of simply existential statements can be read as programs was established by Goedel and Kreisel half a century ago. But the possibility o…
Sound and Complete Typing for lambda-mu
Steffen van Bakel
In this paper we define intersection and union type assignment for Parigot's calculus lambda-mu. We show that this notion is complete (i.e. closed under subject-expansion), and sho…