Publications

On Programming Languages:

Q. Carbonneaux, N. Zilberstein, C. Klee, P. O'Hearn, F. Zappa Nardelli: Applying Formal Verification to Microkernel IPC at Meta, in CPP'22. [pdf]

T. Bastian, F. Zappa Nardelli: Fast and Reliable DWARF Stack Unwinding, in OOPSLA 2019. [web]

B. Chung, F. Zappa Nardelli, J. Vitek: Julia's efficient algorithm for subtyping unions and covariant tuples, in ECOOP 2019. [pdf]

F. Zappa Nardelli, J. Belyakova, A. Pelenitsyn, B. Chung, J. Bezanson, J. Vitek: Julia Subtyping: a Rational Reconstruction, in OOPSLA 2018. [web]

B. Chung, P. Li, F. Zappa Nardelli, J. Vitek: A Framework for Object-Oriented Gradual Typing, in ECOOP 2018. [pdf]

G. Richards, F. Zappa Nardelli, J. Vitek: Concrete Types for TypeScript, in ECOOP 2015. [web]

J. Sevcik, V. Vafeiadis, F. Zappa Nardelli, P. Sewell, S. Jagannathan: CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency, Journal of the ACM, Vol. 60, No 3, 2013. [pdf], [web]

V. Vafeiadis, F. Zappa Nardelli: Verifying Fence Elimination Optimisations, in SAS 2011. [pdf]

J. Sevcik, V. Vafeiadis, F. Zappa Nardelli, P. Sewell, S. Jagannathan: Relaxed-Memory Concurrency and Verified Compilation, in POPL 2011. [web]

T. Wrigstad, F. Zappa Nardelli, S. Lebresne, J. Östlund, J. Vitek: Integration of Typed and Untyped Code in a Scripting Language, in POPL 2010. [web]

A. Hobor, A. Appel, F. Zappa Nardelli: Oracle Semantics for Concurrent Separation Logic, in ESOP'08, LNCS 4960. [.pdf]

P. Sewell, J. Leifer, K. Wansbrough, F. Zappa Nardelli, M. Allen-Williams, P. Habouzit, V. Vafeiadis: Acute: High-level programming language design for distributed computation. Journal of Functional Programming, 2007. An extended abstract [.pdf] appeared in ICFP 2005. The long version is available as INRIA Research Report RR-5329, October 2004. A draft of a more detailed description of Acute is available [.pdf]. Also, check the Acute web-page for more material, including the source distribution of the compiler and of the run-time.

On Weak Memory Models:

R. Morisset, F. Zappa Nardelli: Partially Redundant Fence Elimination for x86, ARM and Power processors, in CC'17. [web]

V. Vafeiadis, T. Balabonsky, S. Chakraborty, R. Morisset, F. Zappa Nardelli: Common compiler optimisations are invalid in the C11 memory model and what we can do about it, in POPL'15. [web]

R. Morisset, P. Pawan, F. Zappa Nardelli: Compiler testing via a theory of sound optimisations in the C11/C++11 memory model, in PLDI'13. [.pdf] [web]

N. M. Lê, A. Pop, A. Cohen, F. Zappa Nardelli: Correct and efficient work-stealing for weak memory models, in PPoPP'13. [.pdf] [errata]

P. Sewell, S. Sarkar, S. Owens, F. Zappa Nardelli, M. Myreen: x86-TSO: a rigorous and usable programmer's model for x86 multiprocessors, in Communications of the ACM, Vol. 53, 2010. [.pdf]

F. Zappa Nardelli, P. Sewell, J. Sevcik, S. Sarkar, S. Owens, L. Maranget, M. Batty, J. Alglave: Relaxed Memory Models must be Rigorous, in (EC)² 09. [.pdf]

S. Sarkar, P. Sewell, F. Zappa Nardelli, S. Owens, T. Braibant, M. Myreen, J. Alglave: The Semantics of x86-CC Multiprocessor Machine Code, in POPL 09. [.pdf]

J. Alglave, A. Fox, S. Isthiaq, M. Myreen, S. Sarkar, P. Sewell, F. Zappa Nardelli: The Semantics of Power and ARM Multiprocessor Machine Code, in DAMP 09. [.pdf]

More resources on the project web-page.

On Security:

G. Richards, C. Hammer, F. Zappa Nardelli, S. Jagannathan, J. Vitek: Flexible Access Control for Javascript, in OOPSLA 13. [.pdf]

N. Guts, C. Fournet, F. Zappa Nardelli: Reliable Evidence: Auditability by Typing, in Esorics 2009. [.pdf]

C. Fournet, N. Guts, F. Zappa Nardelli: A Formal Implementation of Value Commitment, in ESOP'08, LNCS 4960. [.pdf]

On Tool Support for Semantics:

S. Owens, P. Böhm, F. Zappa Nardelli, P. Sewell: Lightweight Tools for Heavyweight Semantics, in ITP 2011. [.pdf]

S. Owens, P. Sewell, S. Weirich, F. Zappa Nardelli: Ott or Nott, in WMM 2010. [.pdf]

P. Sewell, F. Zappa Nardelli, S. Owens, G. Peskine, T. Ridge, S. Sarkar, R. Strniša: Ott: Effective Tool Support for the Working Semanticist, in Journal of Functional Programming, 2010. [.pdf] Also in ICFP'07, Most Influential ICFP Paper Award, 2017. [.pdf]

Check the Ott web page and download the current version: 0.25.

On Process Languages:

M. Merro, F. Zappa Nardelli: Behavioral Theory for Mobile Ambients, Journal of the ACM, Vol. 52, No. 6, 2005. [.pdf] This supersedes the preliminary version available as INRIA Research Report RR-5375, November 2004, and the articles Behavioural Theory for Mobile Ambients, appeared in IFIP TCS, 2004, and Bisimulation Proof Methods for Mobile Ambients, Technical Report COGS 2003:1, an extended abstract appeared in ICALP 2003, LNCS 2719 [.ps.gz]. A not-so-short extended abstract of the latter is also available. [.ps.gz].

G. Winskel, F. Zappa Nardelli: new-HOPLA: a Higher-Order Process Language with Name Generation, BRICS RS-04-21. An extended abstract appeared in IFIP TCS, 2004 (also available as UCAM-CL-TR-589).

G. Castagna, J. Vitek, F. Zappa Nardelli: The Seal Calculus, Information and Computation, Volume 201, Issue 1, 2005, [.pdf] . This supersedes the articles by G. Castagna, F. Zappa Nardelli: The Seal Calculus Revisited: Contextual Equivalences and Bisimilarity, in FSTTCS 2002, LNCS 2556, [.ps.gz] and by G. Castagna, G. Ghelli, F. Zappa Nardelli: Typing Mobility in the Seal Calculus, in Concur 2001, LNCS. [.ps.gz]

Dissertations:

My HDR memoir on Reasoning between Programming Languages and Architectures, 2013.

My PhD thesis on the Semantics of Higher-Order Processes, Université Paris 7, 2003.

My master thesis on type systems for Process Calculi, University of Pisa, 2000.

Last update: