Sam Staton

Room FS08 University of Cambridge Computer Laboratory 15 JJ Thomson Avenue Cambridge CB3 0FD (01223) (7)63584 sam.staton at cl.cam.ac.uk

I am a lecturer in the Computer Laboratory in Cambridge. This year I am lecturing Discrete mathematics I (Part 1a), Semantics of programming languages (Part 1b), and Category theory and logic (Part III/MPhil).

My research is in foundations for the semantics of programming languages. I am interested in several areas, including:

• Computational monads and algebraic theories: This line of work stems from the observation that notions of computation can be determined by program equations using techniques from universal algebra. I have presented new algebraic frameworks to analyze program equations for local store, pi-calculus and functional logic programming (LICS 2013 and FOSSACS 2013, also FOSSACS 2010 and MFPS 2009).
• Type theory: I am interested in type theories for effectful computation. In my paper with Paul Levy (POPL 2013) I investigate structure in typed effectful computation using the universal properties from category theory. In my work with Rasmus Møgelberg (CALCO 2011) I have used a linear type theory to analyze the completeness of the state-passing translation.
• Concurrency: My PhD work with Marcelo Fiore involved bringing together different semantic techniques (operational and denotational) for process calculi like the pi-calculus (published at LICS 2006 and 2008, and Inform. Comput. 2006 and Inform. Comput. 2009). Subsequently with Glynn Winskel I analyzed the model of event structures with symmetry (LICS 2010).

Quick biography: Fixed-term lectureship at Cambridge (Jan 2011 — Dec 2013). Researcher on the ANR project Curry-Howard and Concurrency Theory at Lab PPS, Paris (June 2010 — Jan 2011). EPSRC Post-Doctoral Research Fellowship in Theoretical Computer Science, at Cambridge: Mathematical Operational Semantics for Data-Passing Processes (June 2007 — May 2010). Research assistant on EPSRC grant Domain Theory for Concurrency — New Categorical Foundations (Jan 2006 — May 2007). PhD Student with Marcelo Fiore (Oct 2002 — Dec 2006).

Publications and preprints

• D. Ahman and S. Staton. Normalization by evaluation and algebraic effects. To appear in Proceedings of Twenty-Ninth Conference on Mathematical Foundations of Programming Semantics (MFPS 2013).

• S. Staton. Instances of computational effects. To appear in Proceedings of Twenty-Eighth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2013). [preprint: pdf]

• S. Staton. An algebraic presentation of predicate logic. In Proceedings of Sixteenth International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2013), Lecture Notes in Comput. Sci. 7794:401-417. Springer, 2013. doi:10.1007/978-3-642-37075-5_26. [preprint: pdf]

• S. Staton and P. Levy. Universal properties for impure programming languages. In Proceedings of Fortieth ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2013), pages 179-192. doi:10.1145/2429069.2429091. [preprint: pdf]

• R. E. Møgelberg and S. Staton. Linearly-used state in models of call-by-value. In Proceedings of Fourth International Conference on Algebra and Coalgebra in Computer Science (CALCO 2011). Lecture Notes in Comput. Sci. 6859:293-313. doi:10.1007/978-3-642-22944-2_21. [preprint: pdf]

• S. Staton. Relating coalgebraic notions of bisimulation. Logical Methods in Computer Science Vol 7, Issue 1 (March 2011). doi:10.2168/LMCS-7(1:13)2011. arXiv:1101.4223.

• S. Staton and G. Winskel. On the expressivity of symmetry in event structures. In Proceedings of 25th Annual IEEE Symposium on Logic in Computer Science (LICS 2010), pages 392-401. doi:10.1109/LICS.2010.37. [preprint: pdf]

• R. E. Møgelberg and S. Staton. Full abstraction in a metalanguage for state. In Workshop on Syntax and Semantics of Low Level Languages (LOLA 2010). Satellite workshop of LICS 2010.

• T. Altenkirch, P. Levy and S. Staton. Higher order containers. In Proceedings of Computability in Europe (CiE 2010). Lecture Notes in Comput. Sci. 6158:11-20. doi:10.1007/978-3-642-13962-8_2. [preprint: pdf]

• M. P. Fiore and S. Staton. Positive structural operational semantics and monotone distributive laws. Short contribution for 10th International Workshop on Coalgebraic Methods in Computer Science (CMCS 2010). CWI Technical report SEN-1004. [preprint: pdf]

• S. Staton. Completeness for algebraic theories of local state. Proceedings of 13th International Conference on Foundations of Software Science and Computation Structure (FOSSACS 2010). Lecture Notes in Comput. Sci. 6014:48-63. doi:10.1007/978-3-642-12032-9_5. [preprint: pdf]

• S. Staton. Relating coalgebraic notions of bisimulation, with applications to name-passing process calculi. Proceedings of 3rd Conference on Algebra and Coalgebra in Computer Science (CALCO 2009). Lecture Notes in Comput. Sci. 5728:191-205. doi:10.1007/978-3-642-03741-2_14. [preprint: pdf] [video: at uniud.it]

• S. Staton. Two cotensors in one: Presentations of algebraic theories for local state and fresh names. Proceedings of 25th Conference on the Mathematical Foundations of Programming Semantics (MFPS 25). Electron. Notes Theor. Comput. Sci. 249:471-490. 2009. doi:10.1016/j.entcs.2009.07.103. [preprint: pdf]

• S. Staton. Substitution in Structural Operational Semantics and value-passing process calculi. Proceedings of 2nd International Workshop on Theory and Applications of Abstraction, Substitution and Naming (TAASN 2009). [preprint: pdf]

• M. Fiore and S. Staton. A Congruence Rule Format for Name-Passing Process Calculi. Information and Computation Vol 207, Issue 2 (February 2009), Pages 209-236. Special Issue on Structural Operational Semantics. doi:10.1016/j.ic.2007.12.005. [preprint: pdf]

• S. Staton. General Structural Operational Semantics through Categorical Logic. Proceedings of 23rd Annual IEEE Symposium on Logic in Computer Science (LICS 2008), pages 166-177. doi:10.1109/LICS.2008.43. [preprint: pdf]

• S. Staton. Name-Passing Process Calculi: Operational Models and Structural Operational Semantics. PhD thesis. Girton College, Cambridge. Supervised by Marcelo Fiore, and examined by Gordon Plotkin and Andrew Pitts. Computer Laboratory Technical Report UCAM-CL-TR-688. [Thesis summary: pdf]

• M. P. Fiore and S. Staton. A Congruence Rule Format for Name-Passing Process Calculi from Mathematical Operational Semantics. Proceedings of 21st Annual IEEE Symposium on Logic in Computer Science (LICS 2006), pages 49-58. doi:10.1109/LICS.2006.7.  [preprint: pdf]

• M. P. Fiore and S. Staton. Comparing operational models of name-passing process calculi. Information and Computation Vol 204, Issue 4 (April 2006), Pages 524-560. doi:10.1016/j.ic.2005.08.004.  [preprint: pdf]. Preliminary version in Proceedings of 7th International Workshop on Coalgebraic Methods in Computer Science (CMCS'04).  Electron. Notes Theor. Comput. Sci. 106:91-104. doi:10.1016/j.entcs.2004.02.025.  [preprint: pdf]

Other people

• Ohad Kammar is a Research Assistant supported by my grant from the Isaac Newton Trust.
• I supervised Ben Roberts' PhD on information flow security for distributed programming languages.
• I supervised Danel Ahman's MPhil project.

Responsibilities and events