Francisco Ferreira

Research

I am a lecturer 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

• 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óordoba
  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 lightheaded solution for ICFP'12 Programming competition where we abuse C++ template engine and use it as a functional program that runs at compile time.