Greg Morrisett, Tarmo Uustalu
Proceedings of the 18th International Conference on Functional Programming
ICFP, 2013.

@proceedings{ICFP-2013,
	acmid         = "2500365",
	address       = "Boston, Massachusetts, USA",
	editor        = "Greg Morrisett and Tarmo Uustalu",
	isbn          = "978-1-4503-2326-0",
	publisher     = "{ACM}",
	title         = "{Proceedings of the 18th International Conference on Functional Programming}",
	year          = 2013,
}

Contents (42 items)

7 ×#functional
7 ×#programming
4 ×#higher-order
4 ×#recursion
3 ×#algebra
3 ×#composition
3 ×#hoare
3 ×#monad
3 ×#reasoning
3 ×#verification

ICFP-2013-Norell #dependent type #interactive #programming

Interactive programming with dependent types (UN), pp. 1–2.

ICFP-2013-TraytelN #regular expression #word

Verified decision procedures for MSO on words based on derivatives of regular expressions (DT, TN), pp. 3–12.

ICFP-2013-BroadbentCHS #approach #higher-order #named #verification

C-SHORe: a collapsible approach to higher-order verification (CHB, AC, MH, OS), pp. 13–24.

ICFP-2013-PetersenOG #automation #haskell

Automatic SIMD vectorization for Haskell (LP, DAO, NG), pp. 25–36.

ICFP-2013-MainlandLJ

Exploiting vector instructions with generalized stream fusio (GM, RL, SLPJ), pp. 37–48.

ICFP-2013-McDonellCKL #functional #gpu #optimisation #source code

Optimising purely functional GPU programs (TLM, MMTC, GK, BL), pp. 49–60.

ICFP-2013-BernardyM

Type-theory in color (JPB, GM), pp. 61–72.

ICFP-2013-DevrieseP #metaprogramming

Typed syntactic meta-programming (DD, FP), pp. 73–86.

ICFP-2013-ZilianiDKNV #coq #monad #named #programming

Mtac: a monad for typed tactic programming in Coq (BZ, DD, NRK, AN, VV), pp. 87–100.

ICFP-2013-Dolan #algebra #functional #linear #using

Fun with semirings: a functional pearl on the abuse of linear algebra (SD), pp. 101–110.

ICFP-2013-BernardyC #context-free grammar #divide and conquer #parsing #performance

Efficient divide-and-conquer parsing of practical context-free languages (JPB, KC), pp. 111–122.

ICFP-2013-Mairson #functional #geometry

Functional geometry and the Traité de Lutherie: functional pearl (HGM), pp. 123–132.

ICFP-2013-Brady #algebra #dependent type #programming #reasoning

Programming and reasoning with algebraic effects and dependent types (EB), pp. 133–144.

ICFP-2013-KammarLO

Handlers in action (OK, SL, NO), pp. 145–158.

ICFP-2013-Jones

Computer science as a school subject (SLPJ), pp. 159–160.

ICFP-2013-Schmidt-SchaussS #correctness #haskell #implementation

Correctness of an STM Haskell implementation (MSS, DS), pp. 161–172.

ICFP-2013-PottierP #programming

Programming with permissions in Mezzo (FP, JP), pp. 173–184.

ICFP-2013-AbelP #approach #pattern matching #recursion #termination

Wellfounded recursion with copatterns: a unified approach to termination and productivity (AA, BP), pp. 185–196.

ICFP-2013-AtkeyM #effectiveness #recursion

Productive coprogramming with guarded recursion (RA, CM), pp. 197–208.

ICFP-2013-HinzeWG #recursion

Unifying structured recursion schemes (RH, NW, JG), pp. 209–220.

ICFP-2013-Krishnaswami #functional #higher-order #programming

Higher-order functional reactive programming without spacetime leaks (NRK), pp. 221–232.

ICFP-2013-Jeffrey #functional #liveness #programming

Functional reactive programming with liveness guarantees (AJ), pp. 233–244.

ICFP-2013-Morihata #parallel #theorem

A short cut to parallelization theorems (AM), pp. 245–256.

ICFP-2013-AxelssonC #functional #higher-order #source code #syntax #using

Using circular programs for higher-order syntax: functional pearl (EA, KC), pp. 257–262.

ICFP-2013-Balabonski

Weak optimality, and the meaning of sharing (TB), pp. 263–274.

ICFP-2013-WeirichHE #similarity

System FC with explicit kind equality (SW, JH, RAE), pp. 275–286.

ICFP-2013-SculthorpeBGG #problem

The constrained-monad problem (NS, JB, GG, AG), pp. 287–298.

ICFP-2013-SvenningssonS #composition #embedded #monad

Simple and compositional reification of monadic embedded languages (JS, BJS), pp. 299–304.

ICFP-2013-HidakaAHKN #graph #order #query #recursion

Structural recursion for querying ordered graphs (SH, KA, ZH, HK, KN), pp. 305–318.

ICFP-2013-DelawareKSO #composition #monad

Modular monadic meta-theory (BD, SK, TS, BCdSO), pp. 319–330.

ICFP-2013-LorenzenE #automation #composition #verification

Modular and automated type-soundness verification for language extensions (FL, SE), pp. 331–342.

ICFP-2013-KeepD #compilation #development #framework

A nanopass framework for commercial compiler development (AWK, RKD), pp. 343–350.

ICFP-2013-St-AmourT #case study #experience #random testing #testing

Experience report: applying random testing to a base type environment (VSA, NT), pp. 351–356.

ICFP-2013-PetersenGDAD #case study #experience #functional #programming

Experience report: functional programming of mHealth applications (CP, MG, DTD, JMA, GAD), pp. 357–362.

ICFP-2013-DelbiancoN #algebra #continuation #hoare #reasoning

Hoare-style reasoning with (algebraic) continuations (GAD, AN), pp. 363–376.

ICFP-2013-TuronDB #concurrent #higher-order #hoare #logic #reasoning #refinement

Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency (AT, DD, LB), pp. 377–390.

ICFP-2013-Chlipala #generative #hoare #logic #metaprogramming #verification

The bedrock structured programming system: combining generative metaprogramming and hoare logic in an extensible program verifier (AC), pp. 391–402.

ICFP-2013-CheneyLW #query

A practical theory of language-integrated query (JC, SL, PW), pp. 403–416.

ICFP-2013-Garcia

Calculating threesomes, with blame (RG), pp. 417–428.

ICFP-2013-DunfieldK #bidirectional #morphism #polymorphism #rank

Complete and easy bidirectional typechecking for higher-rank polymorphism (JD, NRK), pp. 429–442.

ICFP-2013-JohnsonLMH #automaton #optimisation

Optimizing abstract abstract machines (JIJ, NL, MM, DVH), pp. 443–454.

ICFP-2013-HritcuHPSVAL #testing

Testing noninterference, quickly (CH, JH, BCP, ASZ, DV, AAdA, LL), pp. 455–468.