P.B.Levy. Call-by-push-value [ps, pdf] PhD thesis, Queen Mary, University of London, 2001. Greatly revised and simplified version is the following:
P.B,Levy. Call-by-push-value. A functional/imperative synthesis, Semantic Structures in Computation, © Springer, 2004.
P.B.Levy. Adjunction models for call-by-push-value with stacks [ps] Proceedings, Category Theory in Computer Science 2002, Ottawa, August 2002, ENTCS vol. 69, article 13 © Elsevier.
P.B.Levy. Adjunction models for call-by-push-value with stacks [pdf], Theory and Applications of Categories volume 14 (2005), article 5 (pages 75-110).
P.B.Levy. Possible world semantics for general storage in call-by-value [ps] LNCS vol. 2471 , J. Bradfield ed., Proceedings, Computer Science Logic, Edinburgh, September 2002, pages 232-246 © Springer.
P.B.Levy, A.J.Power and H.Thielecke. Modelling environments in call-by-value programming languages [ps] © Elsevier, Information and Computation, 2003, vol. 185, pp. 182-210.
J.M.E.Hyland, P.B.Levy, G.D.Plotkin and A.J.Power. Combining continuations with other effects [ps] 4th ACM-SIGPLAN Continuation Workshop, Venice, Italy, January 2004.
P.B.Levy. Infinite trace equivalence [pdf] Proceedings, 21st Conference on the Mathematical Foundations of Programming Semantics, Birmingham, U.K., June 2005, ENTCS volume 155 (published 2006), pages 467-496 (article 22) © Elsevier.
P.B.Levy. Jumping semantics for call-by-push-value [pdf], O. Danvy and H. Thielecke eds., Proceedings, KAZAM Workshop, Birmingham, U.K., June 2005, University of Birmingham technical report CSR-06-10 (appeared 2006), pages 27-40.
P.B.Levy. Infinitary Howe's method [pdf] Proceedings, 8th International Workshop on Coalgebraic Methods in Computer Science, Vienna, Austria, March 2006, ENTCS volume 164, issue 1, pages 85-104 (article 6) © Elsevier.
P.B.Levy. Monads and adjunctions for global exceptions [pdf] Proceedings, 22nd Conference on the Mathematical Foundations of Programming Semantics, Genoa, Italy, May 2006, Entcs, volume 158, pages 261-287 (article 14) © Elsevier.
P.B.Levy. Jumbo lambda-calculus [pdf] LNCS vol. 4052, M. Bugliesi, B. Preneel, V. Sassone, I. Wegener (eds.), Proceedings, 33rd International Colloquium on Automata, Languages and Programming, Track B, Venice, Italy, July 2006, Part 2, pages 444-455 © Springer.
P.B.Levy. Call-by-push-value: decomposing call-by-value and call-by-name [pdf], Higher-Order and Symbolic Computation, vol. 19(4), pages 377-414, December 2006 © Springer.
J.M.E.Hyland, P.B.Levy, G.D.Plotkin and A.J.Power. Combining algebraic effects with continuations [pdf], Festschrift for John Reynolds' 70th birthday, Theoretical Computer Science, vol. 375 (1-3), pages 20-40, May 2007 © Elsevier.
P.B.Levy. Amb breaks well-pointedness, ground amb doesn't [pdf]. Proceedings of the 23rd conference on the Mathematical Foundations of Programming Semantics, New Orleans, April 2007, ENTCS, volume 173, pages 221-239 (article 14) © Elsevier.
S.B.Lassen and P.B.Levy. Typed normal form bisimulation [pdf]. LNCS vol. 4646, J. Duparc and T. A. Henzinger (eds.), Proceedings of the 6th EACSL Annual Conference on Computer Science and Logic (CSL 07), Lausanne, Switzerland, September 2007, pages 283-297 © Springer.
P.B.Levy. Infinite trace equivalence [pdf] Annals of Pure and Applied Logic, vol. 151(2-3), pages 170-198, February 2008, special issue for for GaLoP 2005 © Elsevier.
P.B.Levy. Global state considered helpful [pdf] Proceedings, 24th conference on the Mathematical Foundations of Programming Semantics, University of Pennsylvania, Philadelphia PA USA, May 2008, ENTCS, volume 218, pages 241-259 (article 15) © Elsevier.
S.B.Lassen and P.B.Levy. Typed normal form bisimulation for parametric polymorphism [pdf] Proceedings, 23rd Annual IEEE Syposium on Logic in Computer Science, Carnegie Mellon University, Pittsburgh PA USA, June 2008, pages 341-352.
P.B.Levy and K.Y.Weldemariam. Exploratory functions on nondeterministic strategies, up to lower bisimilarity [pdf] Proceedings, 25th conference on the Mathematical Foundations of Programming Semantics, Oxford UK, April 2009, ENTCS, volume 249, pages 357-375 (article 19) © Elsevier.
T.Altenkirch, P.B.Levy and S.Staton. Higher-order containers [pdf] in Programs, Proofs, Processes 6th Conference on Computability in Europe , Ponta Delgada (Azores), Portugal, July 2010, LNCS vol 6158 pages 11-20, © Springer.
P.B.Levy. Characterizing recursive programs up to bisimilarity [pdf], Proceedings of the 7th Workshop on Fixed Points in Computer Science, Brno, Czech Repulbic, August 2010, HAL-INRIA 00512377 pages 47-52.
P.B.Levy. Similarity Quotients as Final Coalgebras [pdf]. In M.Hofmann (ed.), Proceedings, 14th international conference on Foundations of Software Science and Computation Structures, Saarbruecken, Germany, March-April 2011, LNCS vol. 6604, pages 27-41, © Springer. Here is a long version [pdf] with proofs and additional results.
V.Koutavas, P.B.Levy, E.Summii. From applicative to environmental bisimulation [pdf], Proceedings, 27th conference on the Mathematical Foundations of Programming Semantics, Carnegie Mellon, Pittsburgh, PA, May 2011, ENTCS, volume 276, pages 215-235 (article 12) © Elsevier. (An early version may be found here.)
J.M.Chapman, P.B.Levy, eds. Proceedings of the 4th workshop on Mathematically Structured Functional Programming, Tallinn, Estonia, March 2012. Volume 76 of EPTCS.
L.Aceto, A.Ingólfsdóttir, P.B.Levy, J.Sack. Characteristic formulae: a general approach. Version dated 18 August 2010. Mathematical Structures in Computer Science 22(2), special issue devoted to papers from EXPRESS 2009, pages 125-173, © Cambridge University Press, 2012.
J.Adámek, N.Bowler, P.B.Levy, S.Milius. Coproducts of monads on Set in Proceedings, 27th Annual ACM/IEEE Symposium on Logic in Computer Science, Dubrovnik, Croatia, June 2012, pages 45-54 © IEEE Press. Here is an extended version with proofs.
R.Perera, U.A.Acar, J.Cheney, P.B.Levy. Functional programs that explain their work in Proceedings 17th ACM-SIGPLAN International Conference on Functional Programming, Copenhagen, Denmark, September 2012 © ACM [pdf] (Supplementary technical report)
S.Staton, P.B.Levy. Universal properties for impure programming languages, in Proceedings, Fortieth ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Rome, Italy, January 2013 © ACM [pdf]
P.B.Levy. Martin-Löf clashes with Griffin, operationally [pdf]
P.B.Levy. Infinite trace semantics [ps] Proceedings, 2nd APPSEM II Workshop, Tallinn, Estonia, April 2004.
S.B.Lassen and P.B.Levy. Some parametricity isomorphisms [pdf]
P.B.Levy. Modal properties of recursively defined commands (work in progress) [pdf] to be presented at Domains IX
P.B.Levy. Boolean precongruences [ pdf ]
Adjunction semantics for call-by-push-value [pdf]
Amb breaks well-pointedness, ground amb doesn't [pdf]
Nondeterminism, fixpoints and bisimulation [pdf]
Semantics of nondeterminism [pdf] a talk intended for a general computer science audience
A tutorial on call-by-push-value [pdf] given at the Workshop on Effects and Type Theory
Normal form bisimulation for polymorphism [pdf]
Modal properties of recursive programs work in progress [pdf]
Pointer game semantics for polymorphism (work in progress - presented at GALOP 2010) [pdf]