A. Abel, Normalization for the Simply-Typed Lambda-Calculus in Twelf, Electron. Notes Theor. Comput. Sci, vol.199, pp.3-16, 2008.

C. Andreetta, V. Bégot, J. Berthold, M. Elsman, F. Henglein et al., FinPar: A Parallel Financial Benchmark, 2016.

. C. Archit and . Optim, , vol.13, 2016.

D. Annenkov and M. Elsman, Certified Compilation of Financial Contracts, Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01883559

B. Aydemir, A. Bohannon, and S. Weirich, Nominal Reasoning Techniques in Coq, Electron. Notes Theor. Comput. Sci, vol.174, pp.69-77, 2007.

N. Benton, C. Hur, A. Kennedy, and C. Mcbride, Strongly Typed Term Representations in Coq, J. Autom. Reasoning, vol.49, pp.141-159, 2012.

G. E. Blelloch, Scans as Primitive Parallel Operations. Computers, IEEE Transactions, vol.38, pp.1526-1538, 1989.
DOI : 10.1109/12.42122

E. Guy and . Blelloch, Vector models for data-parallel computing, vol.75, 1990.

M. T. Manuel, G. Chakravarty, S. Keller, T. L. Lee, V. Mcdonell et al., Accelerating Haskell array codes with multicore GPUs, Proceedings of the Sixth Workshop on Declarative Aspects of Multicore Programming, pp.3-14, 2011.

A. Chlipala, C. John, E. Mitchell, and . Moggi, Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Robert Harper, Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '90), pp.341-354, 1990.

R. Harper and C. Stone, Proof, Language, and Interaction, Chapter A Type-theoretic Interpretation of Standard ML, pp.341-387, 2000.

T. Henriksen, M. Dybdal, H. Urms, A. S. Kiehn, D. Gavin et al., APL on GPUs: A TAIL from the Past, Scribbled in Futhark, Procs. of the 5th Int. Workshop on Functional High-Performance Computing (FHPC '16, pp.38-43, 2016.

T. Henriksen, M. Elsman, and C. E. Oancea, Size slicing: a hybrid approach to size inference in Futhark, Proceedings of the 3rd ACM SIGPLAN workshop on Functional high-performance computing, pp.31-42, 2014.

T. Henriksen, K. F. Larsen, and C. E. Oancea, Design and GPGPU Performance of Futhark's Redomap Construct, Proceedings of the 3rd ACM SIGPLAN International Workshop on Libraries, Languages, and Compilers for Array Programming, pp.17-24, 2016.

T. Henriksen, . Cosmin, and . Oancea, Bounds checking: An instance of hybrid analysis, Proceedings of ACM SIGPLAN International Workshop on Libraries, Languages, and Compilers for Array Programming, p.88, 2014.

T. Henriksen, G. W. Niels, M. Serup, F. Elsman, C. E. Henglein et al., Futhark: Purely Functional GPU-programming with Nested Parallelism and In-place Array Updates, Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp.556-571, 2017.
DOI : 10.1145/3140587.3062354

A. Kiel and H. , Higher-Order Functions for a High-Performance Programming Language for GPUs, vol.5, 2018.

K. E. Iverson, A Programming Language, 1962.

S. Joe and F. Y. Kuo, Remark on Algorithm 659: Implementing Sobol's Quasirandom Sequence Generator, ACM Trans. Math. Softw, vol.29, pp.49-57, 2003.

T. Johnsson, Lambda Lifting: Transforming Programs to Recursive Equations, Proceedings of the international conference on Functional Programming Languages and Computer Architecture, pp.190-203, 1985.

T. Rasmus-wriedt-larsen and . Henriksen, Strategies for Regular Segmented Reductions on GPU, Proceedings of the 6th ACM SIGPLAN International Workshop on Functional High-Performance Computing, pp.42-52, 2017.

D. K. Lee, K. Crary, and R. Harper, Towards a Mechanized Metatheory of Standard ML, Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '07), pp.173-184, 2007.

X. Leroy, Applicative Functors and Fully Transparent Higher-order Modules, Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '95), 1995.
DOI : 10.1145/199448.199476

URL : https://hal.archives-ouvertes.fr/hal-01499966

X. Leroy, A Modular Module System, Journal of Functional Programming, vol.10, issue.3, pp.269-303, 2000.
URL : https://hal.archives-ouvertes.fr/inria-00073825

G. Mainland and G. Morrisett, Nikola: Embedding Compiled GPU Functions in Haskell, Proceedings of the Third ACM Haskell Symposium on Haskell, pp.67-78, 2010.

T. L. Mcdonell, M. T. Manuel, G. Chakravarty, B. Keller, and . Lippmeier, Optimising Purely Functional GPU Programs, Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming (ICFP '13), 2013.

R. Milner, M. Tofte, R. Harper, and D. Macqueen, The Definition of Standard ML (Revised), 1997.

S. Najd, S. Lindley, J. Svenningsson, and P. Wadler, Everything Old is New Again: Quoted Domain-specific Languages, Proceedings of the 2016 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM '16), pp.25-36, 2016.
DOI : 10.1145/2847538.2847541

URL : http://arxiv.org/pdf/1507.07264

N. Nystrom, D. White, and K. Das, Firepile: Run-time Compilation for GPUs in Scala, Proceedings of the 10th ACM International Conference on Generative Programming and Component Engineering, pp.107-116, 2011.

, ICFP, Article 97. Publication date, vol.2, 2018.

, Static Interpretation of Higher-Order Modules in Futhark, vol.97, p.31

J. Simon-peyton-jones, J. Eber, and . Seward, Composing Contracts: an Adventure in Financial Engineering (functional pearl), Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP '00), pp.280-292, 2000.

C. Benjamin, A. Pierce, C. Azevedo-de-amorim, M. Casinghino, M. Gaboardi et al., C?at?alinC?at?C?at?alin Hri?cu, Vilhelm Sjöberg, and Brent Yorgey. 2016. Software Foundations. Electronic textbook

A. M. Pitts, Nominal Sets: Names and Symmetry in Computer Science, 2013.

N. Ramsey, K. Fisher, and P. Govereau, An Expressive Language of Signatures, Proceedings of the Tenth ACM SIGPLAN International Conference on Functional Programming (ICFP '05), pp.27-40, 2005.

C. John and . Reynolds, Using Functor Categories to Generate Intermediate Code, Proceedings of the 22Nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '95), pp.25-36, 1995.

A. Rossberg and D. Dreyer, Mixin' Up the ML Module System, ACM Transactions on Programming Languages and Systems, vol.35, issue.2, pp.1-2, 2013.

A. Rossberg, C. V. Russo, and D. Dreyer, F-ing modules, Journal of Functional Programming, vol.24, pp.529-607, 2014.
DOI : 10.1145/1708016.1708028

V. Claudio and . Russo, Non-dependent Types for Standard ML Modules, Proceedings of the International Conference PPDP'99 on Principles and Practice of Declarative Programming (PPDP '99), pp.80-97, 1999.

Z. Shao, Transparent Modules with Fully Syntatic Signatures, Proceedings of the Fourth ACM SIGPLAN International Conference on Functional Programming (ICFP '99), pp.220-232, 1999.

Z. Shao and A. W. Appel, Smartest Recompilation, Proceedings of the 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '93), pp.439-450, 1993.
DOI : 10.1145/158511.158702

M. Steuwer, C. Fensch, S. Lindley, and C. Dubach, Generating Performance Portable Code Using Rewrite Rules: From High-level Functional Expressions to High-performance OpenCL Code, SIGPLAN Not, vol.50, pp.205-217, 2015.

M. Steuwer, T. Remmelg, and C. Dubach, Lift: A Functional Data-parallel IR for High-performance GPU Code Generation, Proceedings of the 2017 International Symposium on Code Generation and Optimization, pp.74-85, 2017.

J. Svensson, Obsidian: GPU Kernel Programming in Haskell, 2011.

D. Swasey, T. Murphy, V. , K. Crary, and R. Harper, A Separate Compilation Extension to Standard ML, Proceedings of the ACM SIGPLAN Workshop on ML (ML '06), 2006.

W. Taha and T. Sheard, MetaML and multi-stage programming with explicit annotations, Theoretical Computer Science, vol.248, 2000.

W. W. Tait, Intensional interpretations of functionals of finite type, Journal of symbolic logic, vol.32, pp.198-212, 1967.

Y. Tan, M. O. Myreen, R. Kumar, A. Fox, S. Owens et al., A New Verified Compiler Backend for CakeML, Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, pp.60-73, 2016.

T. L. Veldhuizen, C++ Templates as Partial Evaluation, Proceedings of the 1999 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation, pp.13-18, 1999.

P. Wadler, Views: A Way for Pattern Matching to Cohabit with Data Abstraction, Proceedings of the 14th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, vol.87, 1987.

P. Wadler and S. Blott, How to Make Ad-hoc Polymorphism Less Ad Hoc, Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '89), pp.60-76, 1989.

L. White, F. Bour, and J. Yallop, Modular implicits, Proceedings of ML/OCaml Workshop 2014, vol.198, pp.22-63, 2015.