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

@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)

6 ×#source code
6 ×#verification
3 ×#compilation
3 ×#composition
3 ×#higher-order
2 ×#abstraction
2 ×#automation
2 ×#data type
2 ×#dependent type
2 ×#generative

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, JÖ, 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.