![](https://dblp.dagstuhl.de/img/logo.ua.320x120.png)
![](https://dblp.dagstuhl.de/img/dropdown.dark.16x16.png)
![](https://dblp.dagstuhl.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp.dagstuhl.de/img/search.dark.16x16.png)
![search dblp](https://dblp.dagstuhl.de/img/search.dark.16x16.png)
default search action
18th ICFP 2013: Boston, MA, USA
- Greg Morrisett, Tarmo Uustalu:
ACM SIGPLAN International Conference on Functional Programming, ICFP'13, Boston, MA, USA - September 25 - 27, 2013. ACM 2013, ISBN 978-1-4503-2326-0
Keynote 1
- Ulf Norell:
Interactive programming with dependent types. 1-2
Verification with grammars and automata
- Dmitriy Traytel
, Tobias Nipkow
:
Verified decision procedures for MSO on words based on derivatives of regular expressions. 3-12 - Christopher H. Broadbent, Arnaud Carayol, Matthew Hague
, Olivier Serre:
C-SHORe: a collapsible approach to higher-order verification. 13-24
Data parallelism
- Leaf Petersen, Dominic A. Orchard
, Neal Glew:
Automatic SIMD vectorization for Haskell. 25-36 - Geoffrey Mainland
, Roman Leshchinskiy, Simon L. Peyton Jones:
Exploiting vector instructions with generalized stream fusio. 37-48 - Trevor L. McDonell
, Manuel M. T. Chakravarty, Gabriele Keller
, Ben Lippmeier:
Optimising purely functional GPU programs. 49-60
Dependent types
- Jean-Philippe Bernardy, Guilhem Moulin:
Type-theory in color. 61-72 - Dominique Devriese
, Frank Piessens:
Typed syntactic meta-programming. 73-86 - Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis
:
Mtac: a monad for typed tactic programming in Coq. 87-100
Fun in the afternoon
- Stephen Dolan:
Fun with semirings: a functional pearl on the abuse of linear algebra. 101-110 - Jean-Philippe Bernardy, Koen Claessen:
Efficient divide-and-conquer parsing of practical context-free languages. 111-122 - Harry G. Mairson:
Functional geometry and the Traité de Lutherie: functional pearl. 123-132
Handling effects
- Edwin C. Brady
:
Programming and reasoning with algebraic effects and dependent types. 133-144 - Ohad Kammar, Sam Lindley
, Nicolas Oury:
Handlers in action. 145-158
Keynote 2
- Simon L. Peyton Jones:
Computer science as a school subject. 159-160
Concurrency
- Manfred Schmidt-Schauß, David Sabel
:
Correctness of an STM Haskell implementation. 161-172 - François Pottier, Jonathan Protzenko:
Programming with permissions in Mezzo. 173-184
(Co-)Recursion
- Andreas Abel, Brigitte Pientka:
Wellfounded recursion with copatterns: a unified approach to termination and productivity. 185-196 - Robert Atkey, Conor McBride:
Productive coprogramming with guarded recursion. 197-208 - Ralf Hinze, Nicolas Wu
, Jeremy Gibbons:
Unifying structured recursion schemes. 209-220
Functional reactive programming
- Neelakantan R. Krishnaswami:
Higher-order functional reactive programming without spacetime leaks. 221-232 - Alan Jeffrey:
Functional reactive programming with liveness guarantees. 233-244 - Akimasa Morihata
:
A short cut to parallelization theorems. 245-256
Lambda-calculus
- Emil Axelsson, Koen Claessen:
Using circular programs for higher-order syntax: functional pearl. 257-262 - Thibaut Balabonski:
Weak optimality, and the meaning of sharing. 263-274 - Stephanie Weirich
, Justin Hsu
, Richard A. Eisenberg
:
System FC with explicit kind equality. 275-286
Monads
- Neil Sculthorpe, Jan Bracker, George Giorgidze, Andy Gill:
The constrained-monad problem. 287-298 - Josef Svenningsson, Bo Joel Svensson:
Simple and compositional reification of monadic embedded languages. 299-304 - Soichiro Hidaka, Kazuyuki Asada, Zhenjiang Hu, Hiroyuki Kato, Keisuke Nakano
:
Structural recursion for querying ordered graphs. 305-318
Modular meta-theory
- Benjamin Delaware, Steven Keuchel
, Tom Schrijvers
, Bruno C. d. S. Oliveira:
Modular monadic meta-theory. 319-330 - Florian Lorenzen, Sebastian Erdweg:
Modular and automated type-soundness verification for language extensions. 331-342
Experience reports
- Andrew W. Keep, R. Kent Dybvig:
A nanopass framework for commercial compiler development. 343-350 - Vincent St-Amour, Neil Toronto:
Experience report: applying random testing to a base type environment. 351-356 - Chris Petersen, Matthias Görges
, Dustin T. Dunsmuir
, John Mark Ansermino
, Guy Albert Dumont
:
Experience report: functional programming of mHealth applications. 357-362
Program logics
- Germán Andrés Delbianco
, Aleksandar Nanevski:
Hoare-style reasoning with (algebraic) continuations. 363-376 - Aaron Turon, Derek Dreyer, Lars Birkedal:
Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency. 377-390 - Adam Chlipala:
The bedrock structured programming system: combining generative metaprogramming and hoare logic in an extensible program verifier. 391-402
Language design
- James Cheney
, Sam Lindley
, Philip Wadler:
A practical theory of language-integrated query. 403-416 - Ronald Garcia:
Calculating threesomes, with blame. 417-428 - Jana Dunfield, Neelakantan R. Krishnaswami:
Complete and easy bidirectional typechecking for higher-rank polymorphism. 429-442
Analysis and optimization
- Dionna Amalie Glaze, Nicholas Labich, Matthew Might, David Van Horn
:
Optimizing abstract abstract machines. 443-454 - Catalin Hritcu, John Hughes, Benjamin C. Pierce, Antal Spector-Zabusky, Dimitrios Vytiniotis, Arthur Azevedo de Amorim, Leonidas Lampropoulos:
Testing noninterference, quickly. 455-468
![](https://dblp.dagstuhl.de/img/cog.dark.24x24.png)
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.