&. Huet, ]. C. Razet-bibliographie, M. Allauzen, and . Mohri, A unified construction of the Glushkov, Follow, and Antimirov automata, pp.110-121, 2006.

V. Antimirov, Partial derivatives of regular expressions and finite automaton constructions, Theoretical Computer Science, vol.155, issue.2, pp.291-319, 1996.
DOI : 10.1016/0304-3975(95)00182-4

G. Berry and R. Sethi, From regular expressions to deterministic automata, Theoretical Computer Science, vol.48, issue.1, pp.117-126, 1986.
DOI : 10.1016/0304-3975(86)90088-5

URL : https://hal.archives-ouvertes.fr/inria-00075904

A. Brüggemann-klein, Regular expressions into finite automata, Theoretical Computer Science, vol.120, issue.2, pp.197-213, 1993.
DOI : 10.1016/0304-3975(93)90287-4

J. A. Brzozowski, Derivatives of Regular Expressions, Journal of the ACM, vol.11, issue.4, pp.481-494, 1964.
DOI : 10.1145/321239.321249

J. Champarnaud, F. Nicart, and D. Ziadi, Computing the Follow Automaton of an Expression, CIAA, pp.90-101, 2004.
DOI : 10.1007/978-3-540-30500-2_9

J. Champarnaud and D. Ziadi, Computing the Equation Automaton of a Regular Expression in O(s 2) Space and Time, In CPM, pp.157-168, 2001.
DOI : 10.1007/3-540-48194-X_15

S. Eilenberg, Automata, Languages, and Machines, volume A, 1974.

G. Huet, Confluent reductions: Abstract properties and applications to term rewriting systems, J. ACM, vol.274, pp.797-821, 1980.
DOI : 10.1109/sfcs.1977.9

G. Huet, The Zen computational linguistics toolkit: Lexicon structures and morphology computations using a modular functional programming language, Tutorial, Language Engineering Conference LEC'2002, 2002.

G. Huet, A functional toolkit for morphological and phonological processing, application to a Sanskrit tagger, Journal of Functional Programming, vol.15, issue.4, pp.573-614, 2005.
DOI : 10.1017/S0956796804005416

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

G. Huet and B. Razet, The Reactive Engine for Modular Transducers, Algebra, Meaning and Computation, Essays Dedicated to Joseph A. Goguen on the Occasion of His 65th Birthday, pp.355-374, 2006.
DOI : 10.1007/11780274_19

L. Ilie and S. Yu, Follow automata, Information and Computation, vol.186, issue.1, pp.140-162, 2003.
DOI : 10.1016/S0890-5401(03)00090-7

URL : http://doi.org/10.1016/s0890-5401(03)00090-7

D. Kozen, On Action Algebras, Logic and Information Flow, pp.78-88, 1994.
DOI : 10.7146/dpb.v21i381.6613

V. Pratt, Action logic and pure induction, Workshop on Logics in Artificial Intelligence, 1991.
DOI : 10.1007/BFb0018436

URL : http://boole.stanford.edu/pub/jelia.pdf

B. Razet, Finite Eilenberg Machines, Proceedings of CIIA 2008, pp.242-251, 2008.
DOI : 10.1007/978-3-540-70844-5_25

URL : https://hal.archives-ouvertes.fr/inria-00257354

B. Razet, Simulating Finite Eilenberg Machines with a Reactive Engine, Proceedings of MSFP 2008, 2008.
DOI : 10.1016/j.entcs.2011.02.019

K. Thompson, Programming Techniques: Regular expression search algorithm, Communications of the ACM, vol.11, issue.6, pp.419-422, 1968.
DOI : 10.1145/363347.363387

D. Benza, M. Cosnard, L. Liquori, and M. Vesin, Arigatoni: A Simple Programmable Overlay Network, IEEE John Vincent Atanasoff 2006 International Symposium on Modern Computing (JVA'06), pp.82-91, 2006.
DOI : 10.1109/JVA.2006.7

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

J. Billings, P. Sewell, M. Shinwell, and R. Strni?a, Type-safe distributed programming for OCaml, Proceedings of the 2006 workshop on ML , ML '06, pp.20-31, 2006.
DOI : 10.1145/1159876.1159881

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.61.9966

D. Andrew, B. J. Birrell, and . Nelson, Implementing remote procedure calls, ACM Trans. Comput. Syst, vol.2, issue.1, pp.39-59, 1984.

C. Courbis, P. Degenne, A. Fau, and D. Parigot, Un modèle abstrait de composants adaptables. revue TSI, Composants et adaptabilité, 2004.
DOI : 10.3166/tsi.23.231-252

C. Fournet, C. Laneve, L. Maranget, and D. Rémy, Implicit typing ?? la ML for the join-calculus, CONCUR '97 : Proceedings of the 8th International Conference on Concurrency Theory, pp.196-212, 1997.
DOI : 10.1007/3-540-63141-0_14

J. Furuse and P. Weis, Entrées/sorties de valeurs en caml, Journées francophones des langages applicatifs, pp.79-98, 2000.

G. Henry, M. Mauny, and E. Chailloux, Typer la dé-sérialisation sans sérialiser les types, Journées francophones des langages applicatifs, pp.133-146, 2006.
DOI : 10.3166/tsi.26.1067-1090

URL : http://arxiv.org/abs/0705.1452

M. Odersky and P. Wadler, Pizza into Java, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '97, pp.146-159, 1997.
DOI : 10.1145/263699.263715

I. Stoica, R. Morris, D. Karger, M. F. Kaashoek, and H. Balakrishnan, Chord, ACM SIGCOMM Computer Communication Review, vol.31, issue.4, pp.149-160, 2001.
DOI : 10.1145/964723.383071

. Sun, Java remote method invocation -distributed computing for java. white paper, 1998.

P. Cousot and R. Cousot, Abstract interpretation, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '77, pp.238-252, 1977.
DOI : 10.1145/512950.512973

URL : https://hal.archives-ouvertes.fr/inria-00528590

P. Cuoq and D. Doligez, Hashconsing in an Incrementally Garbage-Collected System, A Story of Weak Pointers and Hashconsing in OCaml 3.10.2, In ACM SIGPLAN Workshop on ML, 2008.

P. Cuoq and V. Prevosto, Documentation of Frama-C's value analysis plug-in, Octobre, 2008.

A. P. Ershov, On programming of arithmetic operations, Communications of the ACM, vol.1, issue.8, pp.3-6, 1958.
DOI : 10.1145/368892.368907

E. Goto, Monocopy and Associative Algorithms in Extended Lisp, 1974.

X. Leroy, Manifest types, modules, and separate compilation, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '94, pp.109-122, 1994.
DOI : 10.1145/174675.176926

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

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, pp.142-153, 1995.
DOI : 10.1145/199448.199476

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

X. Leroy, Abstract, Journal of Functional Programming, vol.6, issue.05, pp.667-698, 1996.
DOI : 10.1017/S0956796800001933

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

X. Leroy, A modular module system, Journal of Functional Programming, vol.10, issue.3, pp.269-303, 2000.
DOI : 10.1017/S0956796800003683

URL : https://hal.archives-ouvertes.fr/inria-00073825

X. Leroy, D. Doligez, and J. Garrigue, Didier Rémy, and Jérôme Vouillon). The Objective Caml System

D. Michie, Memo functions : a language feature with "rote-learning" properties. Research Memorandum MIP-R-29, Department of Machine Intelligence & Perception, 1967.

D. Michie, ???Memo??? Functions and Machine Learning, Nature, vol.218, issue.5138, pp.19-22, 1968.
DOI : 10.1038/218306c0

J. Peeters, D. Sol, and . Lsl, Participation à un outil de vérification de programmes, 2008.

N. Ramsey, ML Module Mania: A Type-Safe, Separately Compiled, Extensible Interpreter, Electronic Notes in Theoretical Computer Science, vol.148, issue.2, 2005.
DOI : 10.1016/j.entcs.2005.11.045

J. Signoles, Calcul statique des applications de modules paramétrés, Journées Francophones des Langages Applicatifs, pp.21-36, 2003.

J. Signoles, Une approche fonctionnelle du modèle vue-contrôleur, Journées Francophones des Langages Applicatifs, 2005.

J. Signoles and V. Prevosto, Frama-C Plug-in Development Guide, 2008.

M. Weiser, Program slices : formal, psychological, and practical investigations of an automatic program abstraction method, 1979.

M. Weiser, Program Slicing, 5th International Conference on Software Engineering, pp.439-449, 1981.
DOI : 10.1109/TSE.1984.5010248

G. Amdahl, Validity of the single-processor approach to achieving large-scale computing requirements, Computer Design, vol.6, issue.12, pp.39-40, 1967.

H. Boehm, A. J. Demers, and S. Shenker, Mostly parallel garbage collection, PLDI, pp.157-164, 1991.
DOI : 10.1145/113446.113459

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.4445

S. Borkar, Thousand core chips ? A technology perspective, DAC, pp.746-749, 2007.
DOI : 10.1109/dac.2007.375263

M. T. Manuel, R. Chakravarty, S. P. Leshchinskiy, G. Jones, S. Keller et al., Data parallel haskell : a status report, DAMP '07 : Proceedings of the 2007 workshop on Declarative aspects of multicore programming, pp.10-18, 2007.

L. Chang, Y. Choi, J. Kedzierski, N. Lindert, P. Xuan et al., Moore's law lives on [cmos transistors]. Circuits and Devices Magazine, pp.35-42, 2003.

I. Murray and . Cole, Algorithmic Skeletons : Structured Management of Parallel Computation. Research Monographs in Parallel and Distributed Computing, 1989.

S. Conchon and F. L. Fessant, Jocaml: mobile agents for Objective-Caml, Proceedings. First and Third International Symposium on Agent Systems Applications, and Mobile Agents, pp.22-29, 1999.
DOI : 10.1109/ASAMA.1999.805390

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.34.9051

D. Doligez and G. Gonthier, Portable, unobtrusive garbage collection for multiprocessor systems, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '94, pp.70-83, 1994.
DOI : 10.1145/174675.174673

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.52.4710

D. Doligez and X. Leroy, A concurrent, generational garbage collector for a multithreaded implementation of ML, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '93, pp.113-123, 1993.
DOI : 10.1145/158511.158611

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

U. Drepper, What every programmer should know about memory, 2007.

R. , K. Dybvig, D. Eby, and C. Bruggeman, Don't stop the BIBOP : Flexible, and efficient storage management for dynamically-typed languages, 1994.

R. A. Maclachlan, Design of CMU Common Lisp, 2003.

R. Halstead, Implementation of multilisp, Proceedings of the 1984 ACM Symposium on LISP and functional programming , LFP '84, 1984.
DOI : 10.1145/800055.802017

M. Jones and P. Hudak, Implicit and explicit parallel programming in haskell

E. Donald and . Knuth, Interview with Donald Knuth, 2008.

E. and U. Kriegel, A conservative garbage collector for an eulisp to ASM/C compiler, OOPSLA 1993 Workshop on Memory Management and Garbage Collection, 1993.

J. Niehren, J. Schwinghammer, and G. Smolka, A Concurrent Lambda Calculus with Futures, Lecture Notes in Computer Science, vol.3717, pp.248-263, 2005.
DOI : 10.1007/11559306_14

URL : https://hal.archives-ouvertes.fr/inria-00090434

S. Shah and M. Bull, OpenMP---OpenMP, Proceedings of the 2006 ACM/IEEE conference on Supercomputing , SC '06, 2006.
DOI : 10.1145/1188455.1188469

L. Guy and . Steele, Data representations in PDP-10 MACLISP. Report A. I. MEMO 420, Massachusetts Institute of Technology, A.I. Lab, 1977.

H. Sutter, The free lunch is over : a fundamental turn toward toward concurrency, Dr. Dobb's Journal, 2005.

S. Eker, M. Knapp, K. Laderoute, P. Lincoln, J. Meseguer et al., PATHWAY LOGIC: SYMBOLIC ANALYSIS OF BIOLOGICAL SIGNALING, Biocomputing 2002, pp.400-412, 2002.
DOI : 10.1142/9789812799623_0038

J. Meseguer and G. Rosu, The rewriting logic semantics project, Theoretical Computer Science, vol.373, issue.3, pp.213-237, 2007.
DOI : 10.1016/j.tcs.2006.12.018

M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-oliet et al., All About Maude, A High-Performance Logical Framework, Lecture Notes in Computer Science, vol.4350, 2007.

P. Borovanský, C. Kirchner, H. Kirchner, P. E. Moreau, and C. Ringeissen, An Overview of ELAN, Electronic Notes in Theoretical Computer Science, vol.15, 1998.
DOI : 10.1016/S1571-0661(05)82552-6

R. Diaconescu and K. Futatsugi, Logical foundations of CafeOBJ, Theoretical Computer Science, vol.285, issue.2, pp.289-318, 2002.
DOI : 10.1016/S0304-3975(01)00361-9

J. Meseguer, Membership algebra as a logical framework for equational specification
DOI : 10.1007/3-540-64299-4_26

S. Eker, J. Meseguer, and A. Sridharanarayanan, The Maude LTL Model Checker, Electronic Notes in Theoretical Computer Science, vol.71, 2002.
DOI : 10.1016/S1571-0661(05)82534-4

URL : http://doi.org/10.1016/s1571-0661(05)82534-4

J. Meseguer, M. Palomino, and N. Martí-oliet, Equational Abstractions, Lecture Notes in Computer Science, vol.2741, pp.2-16, 2003.
DOI : 10.1007/978-3-540-45085-6_2

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.183.9812

M. Clavel, M. Palomino, and A. Riesco, Introducing the itp tool : a tutorial, J. Universal Computer Science, vol.12, issue.11, pp.1618-1650, 2006.

R. Bruni and J. Meseguer, Semantic foundations for generalized rewrite theories, Theoretical Computer Science, vol.360, issue.1-3, pp.386-414, 2006.
DOI : 10.1016/j.tcs.2006.04.012

J. Meseguer and P. Thati, Symbolic reachability analysis using narrowing and its application to the verification of cryptographic protocols, WRLA, 2004.

K. Futatsugi, Verifying Specifications with Proof Scores in CafeOBJ, 21st IEEE/ACM International Conference on Automated Software Engineering (ASE'06), pp.3-10, 2006.
DOI : 10.1109/ASE.2006.73

K. Ogata and K. Futatsugi, State Machines as Inductive Types, IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences, vol.90, issue.12, pp.90-2985, 2007.
DOI : 10.1093/ietfec/e90-a.12.2985

W. Kong, T. Seino, K. Futatsugi, and K. Ogata, A lightweight integration of theorem proving and model checking for system verification, 12th Asia-Pacific Software Engineering Conference (APSEC'05), pp.59-66, 2005.
DOI : 10.1109/APSEC.2005.9

K. Ogata, M. Nakano, M. Nakamura, and K. Futatsugi, Chocolat/SMV: A Translator from CafeOBJ into SMV, Sixth International Conference on Parallel and Distributed Computing Applications and Technologies (PDCAT'05), pp.416-420, 2005.
DOI : 10.1109/PDCAT.2005.98

M. Nakamura, W. Kong, K. Ogata, and K. Futatsugi, A Specification Translation from Behavioral Specifications to Rewrite Specifications, IEICE Transactions on Information and Systems, vol.91, issue.5, pp.91-1492, 2008.
DOI : 10.1093/ietisy/e91-d.5.1492

Y. Kesten, O. Maler, M. Marcus, A. Pnueli, and E. Shahar, Symbolic model checking with rich assertional languages, Theoretical Computer Science, vol.256, issue.1-2, pp.93-112, 2001.
DOI : 10.1016/S0304-3975(00)00103-1

A. Pnueli, J. Xu, and L. Zuck, Liveness with (0,1, ???)- Counter Abstraction, Lecture Notes in Computer Science, pp.107-122, 2002.
DOI : 10.1007/3-540-45657-0_9

?. K. Et-un-terme-t-?-t-? and . State, Alors, pour tout terme clos t ? T ?, ?X)t ?? t si et seulement si M(R, t) t : Reachable

A. Abel, Termination checking with types Special Issue : Fixed Points in Computer Science (FICS'03), RAIRO ? Theoretical Informatics and Applications, pp.277-319, 2004.

S. Baro, Conception et implémentation d'un système d'aide à la spécification et à la preuve de programmes ML, 2003.

S. Baro and P. Manoury, Un système x. raisonner formellement sur les programmes ml, JFLA, 2003.

P. Taylor, J. Girard, and Y. Lafont, Proofs and types, 1989.

J. Krivine, Lambda-calcul, types et modèles, 1990.

C. Paulin-mohring, Définitions Inductives en Théorie des Types d'Ordre Supérieur. Habilitation à diriger les recherches, 1996.

J. Wells, Typability and type checking in the second order lambda-calculus are equivalent and undecidable, LICS, 1994.

S. Berghofer, A Constructive Proof of Higman???s Lemma in Isabelle, Types for Proofs and Programs, 2003.
DOI : 10.1007/978-3-540-24849-1_5

S. Berghofer, Proofs, Programs and Executable Specifications in Higher Order Logic, 2003.

Z. Dargaye, Décurryfication certifiée, Journées Françaises sur les Langages Applicatifs JFLA'07, 2007.

H. Benl, Proof theory at work : Program development in the Minlog system Automated Deduction : A Basis for Applications. Volume II, Systems and Implementation Techniques, 1998.

H. Geuvers, Inconsistency of classical logic in type theory, 2001.

W. A. Howard, The formulae-as-types notion of constructions, to H.B. Curry : Essays on Combinatory Logic, Lambda Calculus and Formalism, 1980.

S. C. Kleene, Introduction to Metamathematics, 1952.

C. Kreitz, The Nuprl Proof Development System, Version 5, 2002.

X. Leroy, Formal certification of a compiler back-end or : programming a compiler with a proof assistant, POPL, pp.42-54, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00000963

P. Letouzey, Programmation fonctionnelle certifiée ? L'extraction de programmes dans l'assistant Coq, 2004.

C. Paulin-mohring, Extracting ??'s programs from proofs in the calculus of constructions, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '89, 1989.
DOI : 10.1145/75277.75285

C. Paulin-mohring, Extraction de programmes dans le Calcul des Constructions, Thèse d'université, 1989.
URL : https://hal.archives-ouvertes.fr/tel-00431825

C. Paulin-mohring and B. Werner, Synthesis of ML programs in the system Coq, Journal of Symbolic Computation, vol.15, issue.5-6, pp.607-640, 1993.
DOI : 10.1016/S0747-7171(06)80007-6

T. Amagbegnon, L. Besnard, and P. L. Guernic, Implementation of the data-flow synchronous language signal, Programming Languages Design and Implementation, pp.163-173, 1995.
URL : https://hal.archives-ouvertes.fr/hal-00544128

A. Arnold, Systèmes de transitions et sémantique des processus communicants, 1992.
DOI : 10.1051/ita/1981150201031

URL : http://archive.numdam.org/article/ITA_1981__15_2_103_0.pdf

A. Benveniste, P. Caspi, S. A. Edwards, N. Halbwachs, P. L. Guernic et al., The synchronous languages 12 years later, Proceedings of the IEEE, vol.91, issue.1, 2003.
DOI : 10.1109/JPROC.2002.805826

A. Benveniste and G. Berry, The synchronous approach to reactive and real-time systems, Proceedings of the IEEE, vol.79, issue.9, pp.147-159, 2002.
DOI : 10.1109/5.97297

URL : https://hal.archives-ouvertes.fr/inria-00075115

A. Benveniste, P. L. Guernic, and C. Jacquemot, Synchronous programming with events and relations: the SIGNAL language and its semantics, Science of Computer Programming, vol.16, issue.2, pp.103-149, 1991.
DOI : 10.1016/0167-6423(91)90001-E

URL : http://doi.org/10.1016/0167-6423(91)90001-e

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development Coq'Art : The Calculus of Inductive Constructions, Series : Texts in Theoretical Computer Science. An EATCS Series, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

J. Boucaron, R. De-simone, and J. Millo, Formal methods for scheduling of latency-insensitive designs, EURASIP Journal on Embedded Systems, issue.1, pp.8-8, 2007.
URL : https://hal.archives-ouvertes.fr/hal-00784464

J. Buck, S. Ha, E. Lee, and D. Messerschmitt, Ptolemy: A Framework for Simulating and Prototyping Heterogeneous Systems, special issue on Simulation Software Development, 1994.
DOI : 10.1016/B978-155860702-6/50048-X

P. Caspi, A. Curic, A. Maignan, C. Sofronis, and S. Tripakis, Translating Discrete-Time Simulink to Lustre, ACM Transactions on Embedded Computing Systems, 2005.
DOI : 10.1007/978-3-540-45212-6_7

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.103.7832

A. Cohen, M. Duranton, C. Eisenbeis, C. Pagetti, F. Plateau et al., N -Synchronous Kahn Networks : a Relaxed Model of Synchrony for Real-Time Systems, ACM International Conference on Principles of Programming Languages, 2006.

A. Cohen, L. Mandel, F. Plateau, and M. Pouzet, Abstraction of Clocks in Synchronous Data-Flow Systems, The Sixth ASIAN Symposium on Programming Languages and Systems (APLAS 08), 2008.
DOI : 10.1016/0167-6423(91)90001-E

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

J. Colaço and M. Pouzet, Clocks as First Class Abstract Types, Third International Conference on Embedded Software, 2003.
DOI : 10.1007/978-3-540-45212-6_10

P. Cousot and R. Cousot, Abstract interpretation, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '77, pp.238-252, 1977.
DOI : 10.1145/512950.512973

URL : https://hal.archives-ouvertes.fr/inria-00528590

A. Curic, Implementing Lustre Programs on Distributed Platforms with Real-time Constraints, 2005.

L. Gérard, Des horlogesentì eres pour la répartition de programmes synchrones flot de données, 2008.

N. Halbwachs and L. Mandel, Simulation and Verification of Asynchronous Systems by means of a Synchronous Model, Sixth International Conference on Application of Concurrency to System Design (ACSD'06), 2006.
DOI : 10.1109/ACSD.2006.24

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

E. Lee and D. Messerschmitt, Synchronous dataflow, IEEE Trans. Comput, vol.75, issue.9, 1987.

R. Milner, A theory of type polymorphism in programming, Journal of Computer and System Sciences, vol.17, issue.3, pp.348-375, 1978.
DOI : 10.1016/0022-0000(78)90014-4

R. Milner, Calculi for synchrony and asynchrony, Theoretical Computer Science, vol.25, issue.3, pp.267-310, 1983.
DOI : 10.1016/0304-3975(83)90114-7

URL : http://doi.org/10.1016/0304-3975(83)90114-7

M. Pouzet, Lucid Synchrone, version 3. Tutorial and reference manual Distribution available at : www, 2006.

I. M. Smarandache, T. Gautier, and P. L. Guernic, Validation of mixed signal-alpha real-time systems through affine calculus on clock synchronisation constraints, World Congress on Formal Methods, pp.1364-1383, 1999.
DOI : 10.1007/3-540-48118-4_22

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

M. Irina, P. L. Smarandache, and . Guernic, Affine transformations in SIGNAL and their application in the specification and validation of real-time systems, ARTS, 1997.

C. Sofronis, Embedded Code Generation from High-level Heterogeneous Components, 2006.
URL : https://hal.archives-ouvertes.fr/tel-00329534

J. Vuillemin, On circuits and numbers, IEEE Transactions on Computers, vol.43, issue.8, 1993.
DOI : 10.1109/12.295849

A. Aho, M. Lam, R. Sethi, and J. Ullman, Compilateurs -Principes, techniques et outils, 2ème édition, Pearson Education, 2007.

P. Anderson, T. Reps, and T. Teitelbaum, Design and implementation of a fine-grained software inspection tool, IEEE Transactions on Software Engineering, vol.29, issue.8, 2003.
DOI : 10.1109/TSE.2003.1223646

M. Blume, Dependency analysis for Standard ML, ACM Transactions on Programming Languages and Systems, vol.21, issue.4, 1999.
DOI : 10.1145/325478.325481

X. Leroy, The Objective Caml system release 3, 2008.

L. Eva-van-emben and . Moonen, Java quality assurance by detecting code smells, Ninth Working Conference on Reverse Engineering, 2002.

L. Autres and M. , booléens, couleurs) sont directement représentés en OCaml. L'interface de Mlpost contient aussi un module Command qui définit le type des commandes METAPOST : commandes de dessin, de remplissage

L. Premièrement and . Plupart, des modules présentés sont a priori mutuellement récursifs : par exemple, les transformations s'appliquent à tous les autres objets, donc chaque module contient une fonction val transform : Transform

. Enfin, il est important de noter que Mlpost n'est pas lié à METAPOST de manière intrinsèque. On pourrait facilement ajouter une sortie TikZ, ou même directement une sortie PostScript à condition d'utiliser une technique similaire à celle de METAPOST pour l

L. Auteurs-tiennent-À-remercier and F. Plateau, Yannick Moy et Claude Marché pour leur contribution à Mlpost, Sylvie Boldo pour la suggestion du titre de l'article et les relecteurs pour leurs remarques

E. Jack and . Bresenham, Algorithm for computer control of a digital plotter, IBM Systems Journal, vol.4, issue.1, pp.25-30, 1965.

A. Cohen, L. Mandel, F. Plateau, and M. Pouzet, Abstraction of Clocks in Synchronous Data-Flow Systems, The Sixth ASIAN Symposium on Programming Languages and Systems (APLAS), 2008.
DOI : 10.1016/0167-6423(91)90001-E

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

S. Conchon and J. Filliâtre, Type-Safe Modular Hash-Consing, In ACM SIGPLAN Workshop on ML, 2006.

J. R. Driscoll, N. Sarnak, D. D. Sleator, and R. E. Tarjan, Making data structures persistent, Journal of Computer and System Sciences, vol.38, issue.1, pp.86-124, 1989.
DOI : 10.1016/0022-0000(89)90034-2

URL : http://doi.org/10.1016/0022-0000(89)90034-2

M. Hellmund, R. Hinze, J. Korittky, and M. Kuhlmann, Ferenc Wágner, and Peter Simons. functional METAPOST

C. Glenn and . Reid, PostScript Language Program Design, 1988.