Francesco Zappa Nardelli

36 papers A* 6A 9B 6Journal 10Unranked 4

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