Francesco Zappa Nardelli

Publication Activity (10 Years)

Years Active: 2001-2022
Publications (10 Years): 10

Top Topics

Formal Verification

Computational Power

Computerized Tomography

Bounded Rationality

Top Venues

Proc. ACM Program. Lang.

Dagstuhl Artifacts Ser.

Publications

Quentin Carbonneaux, Noam Zilberstein, Christoph Klee, Peter W. O'Hearn, Francesco Zappa Nardelli
Applying formal verification to microkernel IPC at meta. CPP (2022)
Benjamin Chung, Francesco Zappa Nardelli, Jan Vitek
Julia's Efficient Algorithm for Subtyping Unions and Covariant Tuples (Pearl). ECOOP (2019)
Benjamin Chung, Francesco Zappa Nardelli, Jan Vitek
On Julia's Efficient Algorithm for Subtyping Union Types and Covariant Tuples (Artifact). Dagstuhl Artifacts Ser. 5 (2) (2019)
Théophile Bastian, Stephen Kell, Francesco Zappa Nardelli
Reliable and fast DWARF-based stack unwinding. Proc. ACM Program. Lang. 3 (OOPSLA) (2019)
Benjamin Chung, Paley Li, Francesco Zappa Nardelli, Jan Vitek
KafKa: Gradual Typing for Objects. ECOOP (2018)
Francesco Zappa Nardelli, Julia Belyakova, Artem Pelenitsyn, Benjamin Chung, Jeff Bezanson, Jan Vitek
Julia subtyping: a rational reconstruction. Proc. ACM Program. Lang. 2 (OOPSLA) (2018)
Benjamin Chung, Paley Li, Francesco Zappa Nardelli, Jan Vitek
KafKa: Gradual Typing for Objects (Artifact). Dagstuhl Artifacts Ser. 4 (3) (2018)
Robin Morisset, Francesco Zappa Nardelli
Partially redundant fence elimination for x86, ARM, and power processors. CC (2017)
Gregor Richards, Francesco Zappa Nardelli, Jan Vitek
Concrete Types for TypeScript. ECOOP (2015)
Viktor Vafeiadis, Thibaut Balabonski, Soham Chakraborty, Robin Morisset, Francesco Zappa Nardelli
Common Compiler Optimisations are Invalid in the C11 Memory Model and what we can do about it. POPL (2015)
Jaroslav Sevcík, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, Peter Sewell
CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency. J. ACM 60 (3) (2013)
Robin Morisset, Pankaj Pawan, Francesco Zappa Nardelli
Compiler testing via a theory of sound optimisations in the C11/C++11 memory model. PLDI (2013)
Gregor Richards, Christian Hammer, Francesco Zappa Nardelli, Suresh Jagannathan, Jan Vitek
Flexible access control for javascript. OOPSLA (2013)
Nhat Minh Lê, Antoniu Pop, Albert Cohen, Francesco Zappa Nardelli
Correct and efficient work-stealing for weak memory models. PPOPP (2013)
Jaroslav Sevcík, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, Peter Sewell
Relaxed-memory concurrency and verified compilation. POPL (2011)
Viktor Vafeiadis, Francesco Zappa Nardelli
Verifying Fence Elimination Optimisations. SAS (2011)
Scott Owens, Peter Böhm, Francesco Zappa Nardelli, Peter Sewell
Lem: A Lightweight Tool for Heavyweight Semantics. ITP (2011)
Tobias Wrigstad, Francesco Zappa Nardelli, Sylvain Lebresne, Johan Östlund, Jan Vitek
Integrating typed and untyped code in a scripting language. POPL (2010)
Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli, Magnus O. Myreen
x86-TSO: a rigorous and usable programmer's model for x86 multiprocessors. Commun. ACM 53 (7) (2010)
Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, Rok Strnisa
Ott: Effective tool support for the working semanticist. J. Funct. Program. 20 (1) (2010)
Nataliya Guts, Cédric Fournet, Francesco Zappa Nardelli
Reliable Evidence: Auditability by Typing. ESORICS (2009)
Jade Alglave, Anthony C. J. Fox, Samin Ishtiaq, Magnus O. Myreen, Susmit Sarkar, Peter Sewell, Francesco Zappa Nardelli
The semantics of power and ARM multiprocessor machine code. DAMP (2009)
Susmit Sarkar, Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Tom Ridge, Thomas Braibant, Magnus O. Myreen, Jade Alglave
The semantics of x86-CC multiprocessor machine code. POPL (2009)
Cédric Fournet, Nataliya Guts, Francesco Zappa Nardelli
A Formal Implementation of Value Commitment. ESOP (2008)
Aquinas Hobor, Andrew W. Appel, Francesco Zappa Nardelli
Oracle Semantics for Concurrent Separation Logic. ESOP (2008)
Peter Sewell, James J. Leifer, Keith Wansbrough, Francesco Zappa Nardelli, Mair Allen-Williams, Pierre Habouzit, Viktor Vafeiadis
Acute: High-level programming language design for distributed computation. J. Funct. Program. 17 (4-5) (2007)
Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Tom Ridge, Susmit Sarkar, Rok Strnisa
Ott: effective tool support for the working semanticist. ICFP (2007)
Massimo Merro, Francesco Zappa Nardelli
Behavioral theory for mobile ambients. J. ACM 52 (6) (2005)
Peter Sewell, James J. Leifer, Keith Wansbrough, Francesco Zappa Nardelli, Mair Allen-Williams, Pierre Habouzit, Viktor Vafeiadis
Acute: high-level programming language design for distributed computation. ICFP (2005)
Giuseppe Castagna, Jan Vitek, Francesco Zappa Nardelli
The Seal Calculus. Inf. Comput. 201 (1) (2005)
Massimo Merro, Francesco Zappa Nardelli
Behavioural Theory for Mobile Ambients. IFIP TCS (2004)
Glynn Winskel, Francesco Zappa Nardelli
New-HOPLA: A Higher-order Process Language with Name Generation. IFIP TCS (2004)
Massimo Merro, Francesco Zappa Nardelli
Bisimulation Proof Methods for Mobile Ambients. ICALP (2003)
Giuseppe Castagna, Francesco Zappa Nardelli
The Seal Calculus Revisited: Contextual Equivalence and Bisimilarity. FSTTCS (2002)
Giuseppe Castagna, Giorgio Ghelli, Francesco Zappa Nardelli
Typing Mobility in the Seal Calculus. CONCUR (2001)