Proceedings of the 37th Symposium on Principles of Programming Languages
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter

Manuel V. Hermenegildo, Jens Palsberg
Proceedings of the 37th Symposium on Principles of Programming Languages
POPL, 2010.

PLT
DBLP
Scholar
Full names Links ISxN
@proceedings{POPL-2010,
	acmid         = "1706299",
	address       = "Madrid, Spain",
	editor        = "Manuel V. Hermenegildo and Jens Palsberg",
	isbn          = "978-1-60558-479-9",
	publisher     = "{ACM}",
	title         = "{Proceedings of the 37th Symposium on Principles of Programming Languages}",
	year          = 2010,
}

Contents (41 items)

POPL-2010-GershenfeldDCKGDGS #automaton #configuration management #logic
Reconfigurable asynchronous logic automata: (RALA) (NG, DD, KC, AK, FG, EDD, SG, PSN), pp. 1–6.
POPL-2010-AtigBBM #memory management #modelling #on the #problem #verification
On the verification problem for weak memory models (MFA, AB, SB, MM), pp. 7–18.
POPL-2010-KoskinenPH #transaction
Coarse-grained transactions (EK, MJP, MH), pp. 19–30.
POPL-2010-AttiyaRR #verification
Sequential verification of serializability (HA, GR, NR), pp. 31–42.
POPL-2010-GodefroidNRT #composition #power of #program analysis
Compositional may-must program analysis: unleashing the power of alternation (PG, AVN, SKR, ST), pp. 43–56.
POPL-2010-ChaudhuriGL #analysis #source code
Continuity analysis of programs (SC, SG, RL), pp. 57–70.
POPL-2010-HarrisSIG #program analysis #satisfiability #source code
Program analysis via satisfiability modulo path programs (WRH, SS, FI, AG), pp. 71–82.
POPL-2010-TristanL #pipes and filters #validation
A simple, verified validator for software pipelining (JBT, XL), pp. 83–92.
POPL-2010-Chlipala #compilation #functional
A verified compiler for an impure functional language (AC), pp. 93–106.
POPL-2010-Myreen #compilation
Verified just-in-time compiler on x86 (MOM), pp. 107–118.
POPL-2010-Terauchi #dependent type
Dependent types from counterexamples (TT), pp. 119–130.
POPL-2010-RondonKJ #low level
Low-level liquid types (PMR, MK, RJ), pp. 131–144.
POPL-2010-SchaferM #datalog #type inference
Type inference for datalog with complex type hierarchies (MS, OdM), pp. 145–156.
POPL-2010-Henzinger #correctness
From Boolean to quantitative notions of correctness (TAH), pp. 157–158.
POPL-2010-Pitts
Nominal system T (AMP), pp. 159–170.
POPL-2010-HoborDA #approximate #formal method
A theory of indirection via approximation (AH, RD, AWA), pp. 171–184.
POPL-2010-DreyerNRB #data type #higher-order #logic #relational
A relational modal logic for higher-order stateful ADTs (DD, GN, AR, LB), pp. 185–198.
POPL-2010-SuterDK #abstraction #algebra #data type
Decision procedures for algebraic data types with abstractions (PS, MD, VK), pp. 199–210.
POPL-2010-MagillTLT #abstraction #automation #source code
Automatic numeric abstractions for heap-manipulating programs (SM, MHT, PL, YKT), pp. 211–222.
POPL-2010-JostHLH #higher-order #resource management #source code
Static determination of quantitative resource usage for higher-order programs (SJ, KH, HWL, MH), pp. 223–236.
POPL-2010-MalechaMSW #database #relational #towards
Toward a verified relational database management system (JGM, GM, AS, RW), pp. 237–248.
POPL-2010-PodelskiW
Counterexample-guided focus (AP, TW), pp. 249–260.
POPL-2010-NanevskiVB #source code #verification
Structuring the verification of heap-manipulating programs (AN, VV, JB), pp. 261–274.
POPL-2010-JiaZSW #dependent type #equivalence
Dependent types and program equivalence (LJ, JZ, VS, SW), pp. 275–286.
POPL-2010-Hutchins #type system
Pure subtype systems (DSH), pp. 287–298.
POPL-2010-GayVRGC #composition #distributed #object-oriented #programming
Modular session types for distributed object-oriented programming (SJG, VTV, AR, NG, AZC), pp. 299–312.
POPL-2010-SrivastavaGF #synthesis #verification
From program verification to program synthesis (SS, SG, JSF), pp. 313–326.
POPL-2010-VechevYY #synthesis
Abstraction-guided synthesis of synchronization (MTV, EY, GY), pp. 327–338.
POPL-2010-BodikCGKTBR #nondeterminism #programming
Programming with angelic nondeterminism (RB, SC, JG, DK, NT, SB, CR), pp. 339–352.
POPL-2010-GreenbergPW #contract
Contracts made manifest (MG, BCP, SW), pp. 353–364.
POPL-2010-SiekW
Threesomes, with and without blame (JGS, PW), pp. 365–376.
POPL-2010-WrigstadNLOV #scripting language
Integrating typed and untyped code in a scripting language (TW, FZN, SL, , JV), pp. 377–388.
POPL-2010-TateSL #compilation #generative #optimisation #proving
Generating compiler optimizations from proofs (RT, MS, SL), pp. 389–402.
POPL-2010-DiasR #automation #declarative #generative #using
Automatically generating instruction selectors using declarative machine descriptions (JD, NR), pp. 403–416.
POPL-2010-JimMW #algorithm #semantics
Semantics and algorithms for data-dependent grammars (TJ, YM, DW), pp. 417–430.
POPL-2010-BrobergS #data flow #named
Paralocks: role-based information flow control and beyond (NB, DS), pp. 431–444.
POPL-2010-BhargavanFG #composition #protocol #security #type system #verification
Modular verification of security protocol code by typing (KB, CF, ADG), pp. 445–456.
POPL-2010-MartinHCAC #c #c++ #concurrent #policy #source code
Dynamically checking ownership policies in concurrent c/c++ programs (JPM, MH, MC, PA, MC), pp. 457–470.
POPL-2010-HeizmannHP
Nested interpolants (MH, JH, AP), pp. 471–482.
POPL-2010-Filinski #monad
Monads in action (AF), pp. 483–494.
POPL-2010-KobayashiTU #higher-order #multi #recursion #transducer #verification
Higher-order multi-parameter tree transducers and recursion schemes for program verification (NK, NT, HU), pp. 495–508.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.