;; (call/cc (lambda (c) (0 (c 1)))) in R6RS the expression (call/cc (lambda (c) (0 (c 1)))) returns 1. Proof. Notation Convention: a single pair [] of square brackets indicates a 'hole' whereas a double one [[]] follows a metafunction as its arguments. (store () [(call/cc (lambda (c) (0 (c 1))))]) [6call/cc] -> (store () [((lambda (c) (0 (c 1))) (throw x [x]))]) [6appN] -> (store () [((lambda () (0 ((throw x [x]) 1))))]) [6app0] -> (store () [(begin (0 ((throw x [x]) 1)))]) [6begind] -> (store () [(0 ((throw x [x]) 1))]) [6throw] ... E_1 = (0 []) E_2 = [] mathcalT[[E_1, E_2]] = (begin mathcalS[[E_1]][1] mathcalR[[E_2]]) = (begin 1 []) -> (store () [(begin 1 (values 1))]) [6promote] -> (store () [(begin (values 1) (values 1))]) [6beginc] -> (store () [(begin (values 1))]) [6begind] -> (store () [(values 1)]) QED.