default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDMatthew J. Parkinson
Person information
- affiliation: Microsoft Research
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
Books and Theses
- 2006
[b1]Matthew J. Parkinson:
Local reasoning for Java. University of Cambridge, UK, 2006
Journal Articles
- 2024
- [j9]Jaehwang Jung
, Jeonghyeon Kim, Matthew J. Parkinson, Jeehoon Kang:
Concurrent Immediate Reference Counting. Proc. ACM Program. Lang. 8(PLDI): 151-174 (2024) - 2023
- [j8]Ellen Arvidsson, Elias Castegren, Sylvan Clebsch, Sophia Drossopoulou, James Noble, Matthew J. Parkinson, Tobias Wrigstad:
Reference Capabilities for Flexible Memory Management. Proc. ACM Program. Lang. 7(OOPSLA2): 1363-1393 (2023) - [j7]Luke Cheeseman, Matthew J. Parkinson, Sylvan Clebsch, Marios Kogias, Sophia Drossopoulou, David Chisnall, Tobias Wrigstad, Paul Liétar:
When Concurrency Matters: Behaviour-Oriented Concurrency. Proc. ACM Program. Lang. 7(OOPSLA2): 1531-1560 (2023) - 2017
- [j6]Matthew J. Parkinson, Dimitrios Vytiniotis, Kapil Vaswani, Manuel Costa, Pantazis Deligiannis, Dylan McDermott, Aaron Blankstein, Jonathan Balkind:
Project snowflake: non-blocking safe manual memory management in .NET. Proc. ACM Program. Lang. 1(OOPSLA): 95:1-95:25 (2017) - [j5]Colin S. Gordon, Michael D. Ernst, Dan Grossman, Matthew J. Parkinson:
Verifying Invariants of Lock-Free Data Structures with Rely-Guarantee and Refinement Types. ACM Trans. Program. Lang. Syst. 39(3): 11:1-11:54 (2017) - 2016
- [j4]Mike Dodds, Suresh Jagannathan, Matthew J. Parkinson, Kasper Svendsen, Lars Birkedal:
Verifying Custom Synchronization Constructs Using Higher-Order Separation Logic. ACM Trans. Program. Lang. Syst. 38(2): 4:1-4:72 (2016) - 2012
- [j3]Matthew J. Parkinson, Alexander J. Summers:
The Relationship Between Separation Logic and Implicit Dynamic Frames. Log. Methods Comput. Sci. 8(3) (2012) - [j2]John Hatcliff, Gary T. Leavens, K. Rustan M. Leino, Peter Müller, Matthew J. Parkinson:
Behavioral interface specification languages. ACM Comput. Surv. 44(3): 16:1-16:58 (2012) - 2011
- [j1]Rok Strnisa, Matthew J. Parkinson:
Lightweight Java. Arch. Formal Proofs 2011 (2011)
Conference and Workshop Papers
- 2024
- [c42]Jaehwang Jung, Jeonghyeon Kim, Matthew J. Parkinson, Jeehoon Kang:
Concurrent Immediate Reference Counting (Abstract). HOPC@SPAA 2024 - [c41]Nathaniel Wesley Filardo, Matthew J. Parkinson:
BatchIt: Optimizing Message-Passing Allocators for Producer-Consumer Workloads: An Intellectual Abstract. ISMM 2024: 121-130 - [c40]Matthew J. Parkinson, Sylvan Clebsch, Tobias Wrigstad:
Reference Counting Deeply Immutable Data Structures with Cycles: An Intellectual Abstract. ISMM 2024: 131-141 - 2023
- [c39]Matthew J. Parkinson, Sylvan Clebsch, Ben Simner:
Wait-Free Weak Reference Counting. ISMM 2023: 85-96 - 2019
- [c38]Paul Liétar, Theodore Butler, Sylvan Clebsch, Sophia Drossopoulou, Juliana Franco, Matthew J. Parkinson, Alex Shamis, Christoph M. Wintersteiger, David Chisnall:
snmalloc: a message passing allocator. ISMM 2019: 122-135 - 2017
- [c37]Matt Windsor, Mike Dodds, Ben Simner, Matthew J. Parkinson:
Starling: Lightweight Concurrency Verification with Views. CAV (1) 2017: 544-569 - [c36]Artem Khyzha, Mike Dodds, Alexey Gotsman, Matthew J. Parkinson:
Proving Linearizability Using Partial Orders. ESOP 2017: 639-667 - [c35]Piyus Kedia, Manuel Costa, Matthew J. Parkinson, Kapil Vaswani, Dimitrios Vytiniotis, Aaron Blankstein:
Simple, fast, and safe manual memory management. PLDI 2017: 233-247 - 2016
- [c34]Artem Khyzha, Alexey Gotsman, Matthew J. Parkinson:
A Generic Logic for Proving Linearizability. FM 2016: 426-443 - 2015
- [c33]Eric Koskinen, Matthew J. Parkinson:
The Push/Pull model of transactions. PLDI 2015: 186-195 - 2013
- [c32]Christoph Haase, Samin Ishtiaq, Joël Ouaknine, Matthew J. Parkinson:
SeLoger: A Tool for Graph-Based Reasoning in Separation Logic. CAV 2013: 790-795 - [c31]Kasper Svendsen, Lars Birkedal, Matthew J. Parkinson:
Joins: A Case Study in Modular Specification of a Concurrent Reentrant Higher-Order Library. ECOOP 2013: 327-351 - [c30]Kasper Svendsen, Lars Birkedal, Matthew J. Parkinson:
Modular Reasoning about Separation of Concurrent Data Structures. ESOP 2013: 169-188 - [c29]John Wickerson, Mike Dodds, Matthew J. Parkinson:
Ribbon Proofs for Separation Logic. ESOP 2013: 189-208 - [c28]Thomas Dinsdale-Young, Lars Birkedal, Philippa Gardner, Matthew J. Parkinson, Hongseok Yang:
Views: compositional reasoning for concurrent programs. POPL 2013: 287-300 - 2012
- [c27]Colin S. Gordon, Matthew J. Parkinson, Jared Parsons, Aleks Bromfield, Joe Duffy:
Uniqueness and reference immutability for safe parallelism. OOPSLA 2012: 21-40 - 2011
- [c26]Byron Cook, Christoph Haase, Joël Ouaknine, Matthew J. Parkinson, James Worrell:
Tractable Reasoning in a Fragment of Separation Logic. CONCUR 2011: 235-249 - [c25]Matthew J. Parkinson, Alexander J. Summers:
The Relationship between Separation Logic and Implicit Dynamic Frames. ESOP 2011: 439-458 - [c24]Matko Botincan, Mike Dodds, Alastair F. Donaldson, Matthew J. Parkinson:
Safe asynchronous multicore memory operations. ASE 2011: 153-162 - [c23]Mike Dodds, Suresh Jagannathan, Matthew J. Parkinson:
Modular reasoning for deterministic parallelism. POPL 2011: 259-270 - [c22]Matko Botincan, Mike Dodds, Alastair F. Donaldson, Matthew J. Parkinson:
Automatic safety proofs for asynchronous memory operations. PPoPP 2011: 313-314 - [c21]Daiva Naudziuniene, Matko Botincan, Dino Distefano, Mike Dodds, Radu Grigore, Matthew J. Parkinson:
jStar-eclipse: an IDE for automated verification of Java programs. SIGSOFT FSE 2011: 428-431 - 2010
- [c20]Kasper Svendsen, Lars Birkedal, Matthew J. Parkinson:
Verifying Generics and Delegates. ECOOP 2010: 175-199 - [c19]Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, Matthew J. Parkinson, Viktor Vafeiadis:
Concurrent Abstract Predicates. ECOOP 2010: 504-528 - [c18]John Wickerson, Mike Dodds, Matthew J. Parkinson:
Explicit Stabilisation for Modular Rely-Guarantee Reasoning. ESOP 2010: 610-629 - [c17]Eric Koskinen, Matthew J. Parkinson, Maurice Herlihy:
Coarse-grained transactions. POPL 2010: 19-30 - [c16]Matthew J. Parkinson:
The Next 700 Separation Logics - (Invited Paper). VSTTE 2010: 169-182 - 2009
- [c15]Mike Dodds, Xinyu Feng, Matthew J. Parkinson, Viktor Vafeiadis:
Deny-Guarantee Reasoning. ESOP 2009: 363-377 - [c14]Alexey Gotsman, Byron Cook, Matthew J. Parkinson, Viktor Vafeiadis:
Proving that non-blocking algorithms don't block. POPL 2009: 16-28 - [c13]Matko Botincan, Matthew J. Parkinson, Wolfram Schulte:
Separation Logic Verification of C Programs with an SMT Solver. SSV 2009: 5-23 - 2008
- [c12]Gavin M. Bierman, Matthew J. Parkinson, James Noble:
UpgradeJ: Incremental Typechecking for Class Upgrades. ECOOP 2008: 235-259 - [c11]Ewan D. Tempero, Gavin M. Bierman, James Noble, Matthew J. Parkinson:
From Java To UpgradeJ: An Empirical Study. HotSWUp 2008 - [c10]Dino Distefano, Matthew J. Parkinson:
jStar: towards practical verification for java. OOPSLA 2008: 213-226 - [c9]Matthew J. Parkinson, Gavin M. Bierman:
Separation logic, abstraction and inheritance. POPL 2008: 75-86 - 2007
- [c8]Viktor Vafeiadis, Matthew J. Parkinson:
A Marriage of Rely/Guarantee and Separation Logic. CONCUR 2007: 256-271 - [c7]Rok Strnisa, Peter Sewell, Matthew J. Parkinson:
The java module system: core design and semantic definition. OOPSLA 2007: 499-514 - [c6]Matthew J. Parkinson, Richard Bornat, Peter W. O'Hearn:
Modular verification of a non-blocking stack. POPL 2007: 297-302 - [c5]Cristiano Calcagno, Matthew J. Parkinson, Viktor Vafeiadis:
Modular Safety Checking for Fine-Grained Concurrency. SAS 2007: 233-248 - 2006
- [c4]Matthew J. Parkinson, Richard Bornat, Cristiano Calcagno:
Variables as Resource in Hoare Logics. LICS 2006: 137-146 - 2005
- [c3]Matthew J. Parkinson, Gavin M. Bierman:
Separation logic and abstraction. POPL 2005: 247-258 - [c2]Richard Bornat, Cristiano Calcagno, Peter W. O'Hearn, Matthew J. Parkinson:
Permission accounting in separation logic. POPL 2005: 259-270 - 2003
- [c1]Gavin M. Bierman, Matthew J. Parkinson:
Effects and effect inference for a core Java calculus. WOOD 2003: 82-107
Parts in Books or Collections
- 2013
- [p1]Matthew J. Parkinson, Gavin M. Bierman:
Separation Logic for Object-Oriented Programming. Aliasing in Object-Oriented Programming 2013: 366-406
Informal and Other Publications
- 2023
- [i4]Ellen Arvidsson, Elias Castegren, Sylvan Clebsch, Sophia Drossopoulou, James Noble, Matthew J. Parkinson, Tobias Wrigstad:
Reference Capabilities for Flexible Memory Management: Extended Version. CoRR abs/2309.02983 (2023) - 2017
- [i3]Artem Khyzha, Mike Dodds, Alexey Gotsman, Matthew J. Parkinson:
Proving Linearizability Using Partial Orders (Extended Version). CoRR abs/1701.05463 (2017) - 2016
- [i2]Artem Khyzha, Alexey Gotsman, Matthew J. Parkinson:
A Generic Logic for Proving Linearizability (Extended Version). CoRR abs/1609.01171 (2016) - 2015
- [i1]Richard Bornat, Jade Alglave, Matthew J. Parkinson:
New Lace and Arsenic: adventures in weak memory with a program logic. CoRR abs/1512.01416 (2015)
Coauthor Index
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-08-03 21:10 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
