default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID37th POPL 2010: Madrid, Spain
- Manuel V. Hermenegildo, Jens Palsberg:
Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010. ACM 2010, ISBN 978-1-60558-479-9
Invited talk
- Neil Gershenfeld, David Dalrymple, Kailiang Chen, Ara N. Knaian, Forrest Green, Erik D. Demaine, Scott Greenwald, Peter Schmidt-Nielsen:
Reconfigurable asynchronous logic automata: (RALA). 1-6
Concurrency
- Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, Madanlal Musuvathi:
On the verification problem for weak memory models. 7-18 - Eric Koskinen, Matthew J. Parkinson, Maurice Herlihy:
Coarse-grained transactions. 19-30 - Hagit Attiya
, G. Ramalingam, Noam Rinetzky:
Sequential verification of serializability. 31-42
Static analysis I
- Patrice Godefroid, Aditya V. Nori, Sriram K. Rajamani, SaiDeep Tetali:
Compositional may-must program analysis: unleashing the power of alternation. 43-56 - Swarat Chaudhuri, Sumit Gulwani, Roberto Lublinerman:
Continuity analysis of programs. 57-70 - William R. Harris, Sriram Sankaranarayanan, Franjo Ivancic, Aarti Gupta:
Program analysis via satisfiability modulo path programs. 71-82
Verified compilers
- Jean-Baptiste Tristan, Xavier Leroy:
A simple, verified validator for software pipelining. 83-92 - Adam Chlipala:
A verified compiler for an impure functional language. 93-106 - Magnus O. Myreen:
Verified just-in-time compiler on x86. 107-118
Type inference
- Tachio Terauchi:
Dependent types from counterexamples. 119-130 - Patrick Maxim Rondon, Ming Kawaguchi, Ranjit Jhala:
Low-level liquid types. 131-144 - Max Schäfer, Oege de Moor:
Type inference for datalog with complex type hierarchies. 145-156
Invited talk
- Thomas A. Henzinger:
From Boolean to quantitative notions of correctness. 157-158
Reasoning about programs
- Andrew M. Pitts:
Nominal system T. 159-170 - Aquinas Hobor, Robert Dockins, Andrew W. Appel:
A theory of indirection via approximation. 171-184 - Derek Dreyer, Georg Neis, Andreas Rossberg, Lars Birkedal:
A relational modal logic for higher-order stateful ADTs. 185-198
Static analysis II
- Philippe Suter, Mirco Dotta, Viktor Kuncak:
Decision procedures for algebraic data types with abstractions. 199-210 - Stephen Magill, Ming-Hsien Tsai, Peter Lee, Yih-Kuen Tsay:
Automatic numeric abstractions for heap-manipulating programs. 211-222 - Steffen Jost, Kevin Hammond, Hans-Wolfgang Loidl, Martin Hofmann:
Static determination of quantitative resource usage for higher-order programs. 223-236
Verification
- J. Gregory Malecha, Greg Morrisett, Avraham Shinnar, Ryan Wisnesky:
Toward a verified relational database management system. 237-248 - Andreas Podelski, Thomas Wies:
Counterexample-guided focus. 249-260 - Aleksandar Nanevski, Viktor Vafeiadis, Josh Berdine:
Structuring the verification of heap-manipulating programs. 261-274
Types
- Limin Jia, Jianzhou Zhao, Vilhelm Sjöberg, Stephanie Weirich:
Dependent types and program equivalence. 275-286 - DeLesley S. Hutchins:
Pure subtype systems. 287-298 - Simon J. Gay, Vasco Thudichum Vasconcelos, António Ravara, Nils Gesbert, Alexandre Z. Caldeira:
Modular session types for distributed object-oriented programming. 299-312
Program synthesis
- Saurabh Srivastava, Sumit Gulwani, Jeffrey S. Foster:
From program verification to program synthesis. 313-326 - Martin T. Vechev, Eran Yahav, Greta Yorsh:
Abstraction-guided synthesis of synchronization. 327-338 - Rastislav Bodík, Satish Chandra, Joel Galenson, Doug Kimelman, Nicholas Tung, Shaon Barman, Casey Rodarmor:
Programming with angelic nondeterminism. 339-352
Relating and integrating static and dynamic checks
- Michael Greenberg, Benjamin C. Pierce, Stephanie Weirich:
Contracts made manifest. 353-364 - Jeremy G. Siek, Philip Wadler:
Threesomes, with and without blame. 365-376 - Tobias Wrigstad, Francesco Zappa Nardelli, Sylvain Lebresne, Johan Östlund, Jan Vitek:
Integrating typed and untyped code in a scripting language. 377-388
Compilers
- Ross Tate, Michael Stepp, Sorin Lerner:
Generating compiler optimizations from proofs. 389-402 - João Dias, Norman Ramsey:
Automatically generating instruction selectors using declarative machine descriptions. 403-416 - Trevor Jim, Yitzhak Mandelbaum, David Walker:
Semantics and algorithms for data-dependent grammars. 417-430
Security and ownership
- Niklas Broberg, David Sands:
Paralocks: role-based information flow control and beyond. 431-444 - Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon:
Modular verification of security protocol code by typing. 445-456 - Jean-Phillipe Martin, Michael Hicks, Manuel Costa, Periklis Akritidis, Miguel Castro:
Dynamically checking ownership policies in concurrent c/c++ programs. 457-470
Medley
- Matthias Heizmann, Jochen Hoenicke, Andreas Podelski:
Nested interpolants. 471-482 - Andrzej Filinski:
Monads in action. 483-494 - Naoki Kobayashi, Naoshi Tabuchi, Hiroshi Unno:
Higher-order multi-parameter tree transducers and recursion schemes for program verification. 495-508
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.
last updated on 2024-12-08 01:36 CET 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:
