Francisco Ferreira

Research

I am a lecturer (tenure track, equivalent to Assistant Professor) in the department of computer science at Royal Holloway, University of London.
Previously, I was a postdoc RA in the Department of Computing at Imperial College London, working with Nobuko Yoshida.

My main research interests are:

• Types systems and formal logic
• Formal meta-theory
• Concurrency, process calculi and session types
• Temporal logic and other modal logics
• Principled approaches to programming

Publications

• Marco Carbone, David Castro-Perez, Francisco Ferreira, Lorenzo Gheri, Frederik Krogsdal Jacobsen, Alberto Momigliano, Luca Padovani, Alceste Scalas, Dawit Tirore, Martin Vassor, Nobuko Yoshida & Daniel Zackon The Concurrent Calculi Formalisation Benchmark. Coordination, 2024. (Website here.)
• Sung-Shik Jongmans, Francisco Ferreira. Synthetic Behavioural Typing: Sound, Regular Multiparty Sessions via Implicit Local Types. ECOOP 2023.
• Francisco Ferreira, Sung-Shik Jongmans. Oven: Safe and Live Communication Protocols in Scala, using Synthetic Behavioural Type Analysis. ISSTA 2023.
• Adam D. Barwell, Francisco Ferreira, Nobuko Yoshida. CONCUR test-of-time award for the period 1994-97 interview with Uwe Nestmann and Benjamin C. Pierce. J. Log. Algebraic Methods 2022.
• Nobuko Yoshida, Fangyi Zhou, and Francisco Ferreira. Communicating Finite State Machines and an Extensible Toolchain for Multiparty Session Types Fundamentals of Computation Theory, 2021.
• David Castro-Perez, Francisco Ferreira, Lorenzo Gheri, and Nobuko Yoshida. Zooid: A dsl for certified multiparty computation: From mechanised metatheory to certified multiparty processes. PLDI 2021.
• Nobuko Yoshida, Fangyi Zhou, and Francisco Ferreira. Communicating Finite State Machines and an Extensible Toolchain for Multiparty Session Types. FCT 2021.
• Anson Miu, Francisco Ferreira, Nobuko Yoshida, and Fangyi Zhou. Communication-safe web programming in typescript with routed multiparty session types. CC 2021.
• Fangyi Zhou, Francisco Ferreira, Raymond Hu, Rumyana Neykova, and Nobuko Yoshida. Statically verified refinements for multiparty protocols. OOPSLA 2020.
• David Castro, Francisco Ferreira, and Nobuko Yoshida. Emtst: Engineering the meta-theory of session types. TACAS 2020.
• Anson Miu, Francisco Ferreira, Nobuko Yoshida, and Fangyi Zhou. Generating interactive websocket applications in typescript. PLACES 2020.
• Brigitte Pientka, David Thibodeau, Andreas Abel, Francisco Ferreira, and Rebecca Zucchini. A type theory for defining logics and proofs. LICS 2019.
• Francisco Ferreira, David Thibodeau, and Brigitte Pientka. Dependent type theory with contextual types. TYPES 2017.
• My PhD Thesis: Proofs and Programs about Open Terms
• Francisco Ferreira and Brigitte Pientka Programs Using Syntax with First-Class Binders ESOP '17. [Appendix with metathory].
• Francisco Ferreira and Brigitte Pientka Bidirectional Elaboration of Dependently Typed Programs . PPDP '14.
• Andrew Cave, Francisco Ferreira, Prakash Panangaden and Brigitte Pientka. Fair Reactive Programming. POPL'14 [Long version]
• Francisco Ferreira, Stefan Monnier and Brigitte Pientka. Compiling contextual objects: bringing higher-order abstract syntax to programmers PLPV '13

Talks and Posters

• Talk on Programming Logical Relations Proofs at Imperial College, London
• Talk on Compiling Contextual Objects at the Workshop on Formal Meta-Theory for the Parsifal Group at Inria
• Poster Bringing Higher-Order Abstract Syntax to Programmers at ICFP'12 Student Research Competition(SRC). Earned first place.

Industrial Experience

• 2015 — Haskell consultant for Erudite Sofware, Montréal, QC
  Helping develop educative software.
• 2008 to 2009 — Game programming for Bluberi, Drummondville, QC
  Developing software for the gambling industry.
• 2005 to 2008 — Software engineer for Motorola Argentina, Córdoba
  Developing mission-critical software for the telecom industry.

Teaching

• Winter 2013 - (Lecturer) COMP 302: Programming Languages and Paradigms (co-teached with Andrew Cave).
• Fall 2012 - (Teacher assistant) COMP 302: Programming Languages and Paradigms.

Fun and miscelanea

• A lighthearted solution for ICFP'12 Programming competition where we abuse C++ template engine and use it as a functional program that runs at compile time.