![](https://dblp.uni-trier.de/img/logo.ua.320x120.png)
![](https://dblp.uni-trier.de/img/dropdown.dark.16x16.png)
![](https://dblp.uni-trier.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
![search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
default search action
Francesco Zappa Nardelli
Person information
- affiliation: INRIA, France
Refine list
![note](https://dblp.uni-trier.de/img/note-mark.dark.12x12.png)
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2022
- [c25]Quentin Carbonneaux, Noam Zilberstein
, Christoph Klee, Peter W. O'Hearn
, Francesco Zappa Nardelli:
Applying formal verification to microkernel IPC at meta. CPP 2022: 116-129
2010 – 2019
- 2019
- [j10]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): 08:1-08:2 (2019) - [j9]Théophile Bastian, Stephen Kell, Francesco Zappa Nardelli:
Reliable and fast DWARF-based stack unwinding. Proc. ACM Program. Lang. 3(OOPSLA): 146:1-146:24 (2019) - [c24]Benjamin Chung
, Francesco Zappa Nardelli, Jan Vitek:
Julia's Efficient Algorithm for Subtyping Unions and Covariant Tuples (Pearl). ECOOP 2019: 24:1-24:15 - 2018
- [j8]Benjamin Chung, Paley Li, Francesco Zappa Nardelli, Jan Vitek:
KafKa: Gradual Typing for Objects (Artifact). Dagstuhl Artifacts Ser. 4(3): 10:1-10:3 (2018) - [j7]Francesco Zappa Nardelli, Julia Belyakova, Artem Pelenitsyn
, Benjamin Chung
, Jeff Bezanson, Jan Vitek:
Julia subtyping: a rational reconstruction. Proc. ACM Program. Lang. 2(OOPSLA): 113:1-113:27 (2018) - [c23]Benjamin Chung
, Paley Li, Francesco Zappa Nardelli, Jan Vitek:
KafKa: Gradual Typing for Objects. ECOOP 2018: 12:1-12:24 - 2017
- [c22]Robin Morisset, Francesco Zappa Nardelli:
Partially redundant fence elimination for x86, ARM, and power processors. CC 2017: 1-10 - 2015
- [c21]Gregor Richards, Francesco Zappa Nardelli, Jan Vitek:
Concrete Types for TypeScript. ECOOP 2015: 76-100 - [c20]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: 209-220 - 2014
- [b1]Francesco Zappa Nardelli:
Reasoning between Programming Languages and Architectures. École Normale Supérieure, Paris, France, 2014 - 2013
- [j6]Jaroslav Sevcík, Viktor Vafeiadis
, Francesco Zappa Nardelli, Suresh Jagannathan, Peter Sewell
:
CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency. J. ACM 60(3): 22:1-22:50 (2013) - [c19]Gregor Richards, Christian Hammer
, Francesco Zappa Nardelli, Suresh Jagannathan, Jan Vitek:
Flexible access control for javascript. OOPSLA 2013: 305-322 - [c18]Robin Morisset, Pankaj Pawan, Francesco Zappa Nardelli:
Compiler testing via a theory of sound optimisations in the C11/C++11 memory model. PLDI 2013: 187-196 - [c17]Nhat Minh Lê, Antoniu Pop, Albert Cohen, Francesco Zappa Nardelli:
Correct and efficient work-stealing for weak memory models. PPoPP 2013: 69-80 - 2011
- [c16]Scott Owens
, Peter Böhm, Francesco Zappa Nardelli, Peter Sewell
:
Lem: A Lightweight Tool for Heavyweight Semantics. ITP 2011: 363-369 - [c15]Jaroslav Sevcík, Viktor Vafeiadis
, Francesco Zappa Nardelli, Suresh Jagannathan, Peter Sewell
:
Relaxed-memory concurrency and verified compilation. POPL 2011: 43-54 - [c14]Viktor Vafeiadis
, Francesco Zappa Nardelli:
Verifying Fence Elimination Optimisations. SAS 2011: 146-162 - 2010
- [j5]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): 89-97 (2010) - [j4]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): 71-122 (2010) - [c13]Tobias Wrigstad, Francesco Zappa Nardelli, Sylvain Lebresne, Johan Östlund, Jan Vitek:
Integrating typed and untyped code in a scripting language. POPL 2010: 377-388
2000 – 2009
- 2009
- [c12]Nataliya Guts, Cédric Fournet, Francesco Zappa Nardelli:
Reliable Evidence: Auditability by Typing. ESORICS 2009: 168-183 - [c11]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: 13-24 - [c10]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: 379-391 - 2008
- [c9]Aquinas Hobor, Andrew W. Appel
, Francesco Zappa Nardelli:
Oracle Semantics for Concurrent Separation Logic. ESOP 2008: 353-367 - [c8]Cédric Fournet, Nataliya Guts, Francesco Zappa Nardelli:
A Formal Implementation of Value Commitment. ESOP 2008: 383-397 - 2007
- [j3]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): 547-612 (2007) - [c7]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: 1-12 - 2005
- [j2]Giuseppe Castagna, Jan Vitek, Francesco Zappa Nardelli:
The Seal Calculus. Inf. Comput. 201(1): 1-54 (2005) - [j1]Massimo Merro
, Francesco Zappa Nardelli:
Behavioral theory for mobile ambients. J. ACM 52(6): 961-1023 (2005) - [c6]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: 15-26 - 2004
- [c5]Glynn Winskel, Francesco Zappa Nardelli:
New-HOPLA: A Higher-order Process Language with Name Generation. IFIP TCS 2004: 521-534 - [c4]Massimo Merro, Francesco Zappa Nardelli:
Behavioural Theory for Mobile Ambients. IFIP TCS 2004: 549-562 - 2003
- [c3]Massimo Merro, Francesco Zappa Nardelli:
Bisimulation Proof Methods for Mobile Ambients. ICALP 2003: 584-598 - 2002
- [c2]Giuseppe Castagna, Francesco Zappa Nardelli:
The Seal Calculus Revisited: Contextual Equivalence and Bisimilarity. FSTTCS 2002: 85-96 - 2001
- [c1]Giuseppe Castagna, Giorgio Ghelli, Francesco Zappa Nardelli:
Typing Mobility in the Seal Calculus. CONCUR 2001: 82-101
Coauthor Index
![](https://dblp.uni-trier.de/img/cog.dark.24x24.png)
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-05-08 21:53 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint