## Peter Thiemann, Robby Bruce Findler

*Proceedings of the 17th International Conference on Functional Programming*

ICFP, 2012.

@proceedings{ICFP-2012, acmid = "2364527", address = "Copenhagen, Denmark", editor = "Peter Thiemann and Robby Bruce Findler", isbn = "978-1-4503-1054-3", publisher = "{ACM}", title = "{Proceedings of the 17th International Conference on Functional Programming}", year = 2012, }

### Contents (35 items)

- ICFP-2012-McBride #dependent type #programming
- Agda-curious?: an exploration of programming with dependent types (CTM), pp. 1–2.
- ICFP-2012-StewartBA #proving #theorem proving
- Verified heap theorem prover by paramodulation (GS, LB, AWA), pp. 3–14.
- ICFP-2012-Huffman #monad #verification
- Formal verification of monad transformers (BH), pp. 15–16.
- ICFP-2012-Dunfield
- Elaborating intersection and union types (JD), pp. 17–28.
- ICFP-2012-ChenEW #type system #λ-calculus
- An error-tolerant type system for variational λ calculus (SC, ME, EW), pp. 29–40.
- ICFP-2012-KrishnaswamiTDG
- Superficially substructural types (NRK, AT, DD, DG), pp. 41–54.
- ICFP-2012-Mitchell #haskell
- Shake before building: replacing make with haskell (NM), pp. 55–66.
- ICFP-2012-Chitil #contract #lazy evaluation
- Practical typed lazy contracts (OC), pp. 67–76.
- ICFP-2012-OliveiraC #functional #graph #programming
- Functional programming with structured graphs (BCdSO, WRC), pp. 77–88.
- ICFP-2012-Sheard #design #programming #reduction
- Painless programming combining reduction and search: design principles for embedding decision procedures in high-level languages (TES), pp. 89–102.
- ICFP-2012-DagandM
- Transporting functions across ornaments (PÉD, CM), pp. 103–114.
- ICFP-2012-MyreenO #higher-order #logic #ml #synthesis
- Proof-producing synthesis of ML from higher-order logic (MOM, SO), pp. 115–126.
- ICFP-2012-Danielsson #monad #semantics #using
- Operational semantics using the partiality monad (NAD), pp. 127–138.
- ICFP-2012-Olukotun #domain-specific language #embedded #performance
- High performance embedded domain specific languages (KO), pp. 139–140.
- ICFP-2012-SeveriV #finite #normalisation #recursion #type system
- Pure type systems with corecursion on streams: from finite to infinitary normalisation (PS, FJdV), pp. 141–152.
- ICFP-2012-EndrullisHB #complexity #equivalence #infinity #on the #specification
- On the complexity of equivalence of specifications of infinite objects (JE, DH, RB), pp. 153–164.
- ICFP-2012-SimoesVFJH #analysis #automation #functional #lazy evaluation #memory management #source code
- Automatic amortised analysis of dynamic memory allocation for lazy functional programs (HRS, PBV, MF, SJ, KH), pp. 165–176.
- ICFP-2012-EarlSMH #analysis #automaton #higher-order #source code
- Introspective pushdown analysis of higher-order programs (CE, IS, MM, DVH), pp. 177–188.
- ICFP-2012-LaunchburyDDA #multi #performance #protocol
- Efficient lookup-table protocol in secure multiparty computation (JL, ISD, TD, AAM), pp. 189–200.
- ICFP-2012-StefanRBLMM #concurrent #data flow #termination
- Addressing covert termination and timing channels in concurrent information flow systems (DS, AR, PB, AL, JCM, DM), pp. 201–214.
- ICFP-2012-Siederdissen #combinator #performance #programming
- Sneaking around concatMap: efficient combinators for dynamic programming (CHzS), pp. 215–226.
- ICFP-2012-DanielsGR #biology #case study #experience #haskell
- Experience report: Haskell in computational biology (NMD, AG, NR), pp. 227–234.
- ICFP-2012-FoltzerKSSJN #composition #scheduling
- A meta-scheduler for the par-monad: composable scheduling for the heterogeneous cloud (AF, AK, RS, SS, EJ, RN), pp. 235–246.
- ICFP-2012-BergstromR #gpu
- Nested data-parallelism on the gpu (LB, JHR), pp. 247–258.
- ICFP-2012-LippmeierCKLJ #higher-order #performance
- Work efficient higher-order vectorisation (BL, MMTC, GK, RL, SLPJ), pp. 259–270.
- ICFP-2012-Sewell
- Tales from the jungle (PS), pp. 271–272.
- ICFP-2012-Wadler
- Propositions as sessions (PW), pp. 273–286.
- ICFP-2012-HenryMCM #type system
- Typing unmarshalling without marshalling types (GH, MM, EC, PM), pp. 287–298.
- ICFP-2012-JonesFA #domain-specific language
- Deconstraining DSLs (WJ, TF, TORA), pp. 299–310.
- ICFP-2012-Mainland #haskell #metaprogramming
- Explicitly heterogeneous metaprogramming with MetaHaskell (GM), pp. 311–322.
- ICFP-2012-Axelsson #embedded #syntax
- A generic abstract syntax model for embedded languages (EA), pp. 323–334.
- ICFP-2012-PikeWNG #case study #compilation #experience
- Experience report: a do-it-yourself high-assurance compiler (LP, NW, SN, AG), pp. 335–340.
- ICFP-2012-VytiniotisJM #compilation #fault #proving #similarity
- Equality proofs and deferred type errors: a compiler pearl (DV, SLPJ, JPM), pp. 341–352.
- ICFP-2012-NeatherwayRO #algorithm #higher-order #model checking
- A traversal-based algorithm for higher-order model checking (RPN, SJR, CHLO), pp. 353–364.
- ICFP-2012-PereraACL #functional #source code
- Functional programs that explain their work (RP, UAA, JC, PBL), pp. 365–376.

4 ×#higher-order

4 ×#performance

4 ×#programming

3 ×#functional

3 ×#haskell

3 ×#source code

3 ×#type system

2 ×#analysis

2 ×#case study

2 ×#compilation

4 ×#performance

4 ×#programming

3 ×#functional

3 ×#haskell

3 ×#source code

3 ×#type system

2 ×#analysis

2 ×#case study

2 ×#compilation