Typing Mobility in the Seal Calculus. - Giuseppe Castagna; Giorgio Ghelli; Francesco Zappa Nardelli (CONCUR, 2001)

The Seal Calculus Revisited: Contextual Equivalence and Bisimilarity. - Giuseppe Castagna; Francesco Zappa Nardelli (FSTTCS, 2002)

Bisimulation Proof Methods for Mobile Ambients. - Massimo Merro; Francesco Zappa Nardelli (ICALP, 2003)

Behavioural Theory for Mobile Ambients. - Massimo Merro; Francesco Zappa Nardelli (IFIP TCS, 2004)

New-HOPLA: A Higher-order Process Language with Name Generation. - Glynn Winskel; Francesco Zappa Nardelli (IFIP TCS, 2004)

The Seal Calculus. - Giuseppe Castagna; Jan Vitek; Francesco Zappa Nardelli (Inf. Comput., 2005)

Behavioral theory for mobile ambients. - Massimo Merro; Francesco Zappa Nardelli (J. ACM, 2005)

Acute: High-level programming language design for distributed computation. - Peter Sewell; James J. Leifer; Keith Wansbrough; Francesco Zappa Nardelli; Mair Allen-Williams; Pierre Habouzit; Viktor Vafeiadis (J. Funct. Program., 2007)

A Formal Implementation of Value Commitment. - Cédric Fournet; Nataliya Guts; Francesco Zappa Nardelli (ESOP, 2008)

Oracle Semantics for Concurrent Separation Logic. - Aquinas Hobor; Andrew W. Appel; Francesco Zappa Nardelli (ESOP, 2008)

Reliable Evidence: Auditability by Typing. - Nataliya Guts; Cédric Fournet; Francesco Zappa Nardelli (ESORICS, 2009)

The semantics of power and ARM multiprocessor machine code. - Jade Alglave; Anthony C. J. Fox; Samin Ishtiaq; Magnus O. Myreen; Susmit Sarkar; Peter Sewell; Francesco Zappa Nardelli (DAMP, 2009)

The semantics of x86-CC multiprocessor machine code. - Susmit Sarkar; Peter Sewell; Francesco Zappa Nardelli; Scott Owens; Tom Ridge; Thomas Braibant; Magnus O. Myreen; Jade Alglave (POPL, 2009)

Integrating typed and untyped code in a scripting language. - Tobias Wrigstad; Francesco Zappa Nardelli; Sylvain Lebresne; Johan Östlund; Jan Vitek (POPL, 2010)

x86-TSO: a rigorous and usable programmer's model for x86 multiprocessors. - Peter Sewell; Susmit Sarkar; Scott Owens; Francesco Zappa Nardelli; Magnus O. Myreen (Commun. ACM, 2010)

Ott: Effective tool support for the working semanticist. - Peter Sewell; Francesco Zappa Nardelli; Scott Owens; Gilles Peskine; Thomas Ridge; Susmit Sarkar; Rok Strnisa (J. Funct. Program., 2010)

Lem: A Lightweight Tool for Heavyweight Semantics. - Scott Owens; Peter Böhm; Francesco Zappa Nardelli; Peter Sewell (ITP, 2011)

Relaxed-memory concurrency and verified compilation. - Jaroslav Sevcík; Viktor Vafeiadis; Francesco Zappa Nardelli; Suresh Jagannathan; Peter Sewell (POPL, 2011)

Verifying Fence Elimination Optimisations. - Viktor Vafeiadis; Francesco Zappa Nardelli (SAS, 2011)

Flexible access control for javascript. - Gregor Richards; Christian Hammer 001; Francesco Zappa Nardelli; Suresh Jagannathan; Jan Vitek (OOPSLA, 2013)

Compiler testing via a theory of sound optimisations in the C11/C++11 memory model. - Robin Morisset; Pankaj Pawan; Francesco Zappa Nardelli (PLDI, 2013)

Correct and efficient work-stealing for weak memory models. - Nhat Minh Lê; Antoniu Pop; Albert Cohen 001; Francesco Zappa Nardelli (PPoPP, 2013)

CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency. - Jaroslav Sevcík; Viktor Vafeiadis; Francesco Zappa Nardelli; Suresh Jagannathan; Peter Sewell (J. ACM, 2013)

Reasoning between Programming Languages and Architectures. - Francesco Zappa Nardelli (2014)

Concrete Types for TypeScript. - Gregor Richards; Francesco Zappa Nardelli; Jan Vitek (ECOOP, 2015)

Common Compiler Optimisations are Invalid in the C11 Memory Model and what we can do about it. - Viktor Vafeiadis; Thibaut Balabonski; Soham Chakraborty 001; Robin Morisset; Francesco Zappa Nardelli (POPL, 2015)

Partially redundant fence elimination for x86, ARM, and power processors. - Robin Morisset; Francesco Zappa Nardelli (CC, 2017)

KafKa: Gradual Typing for Objects. - Benjamin Chung; Paley Li; Francesco Zappa Nardelli; Jan Vitek (ECOOP, 2018)

KafKa: Gradual Typing for Objects (Artifact). - Benjamin Chung; Paley Li; Francesco Zappa Nardelli; Jan Vitek (Dagstuhl Artifacts Ser., 2018)

Julia subtyping: a rational reconstruction. - Francesco Zappa Nardelli; Julia Belyakova; Artem Pelenitsyn; Benjamin Chung; Jeff Bezanson; Jan Vitek (Proc. ACM Program. Lang., 2018)

Julia's Efficient Algorithm for Subtyping Unions and Covariant Tuples (Pearl). - Benjamin Chung; Francesco Zappa Nardelli; Jan Vitek (ECOOP, 2019)

On Julia's Efficient Algorithm for Subtyping Union Types and Covariant Tuples (Artifact). - Benjamin Chung; Francesco Zappa Nardelli; Jan Vitek (Dagstuhl Artifacts Ser., 2019)

Reliable and fast DWARF-based stack unwinding. - Théophile Bastian; Stephen Kell; Francesco Zappa Nardelli (Proc. ACM Program. Lang., 2019)

Applying formal verification to microkernel IPC at meta. - Quentin Carbonneaux; Noam Zilberstein; Christoph Klee; Peter W. O'Hearn; Francesco Zappa Nardelli (CPP, 2022)