From Semantics to Computer Science

Essays in Honour of Gilles Kahn

From Semantics to Computer Science

Gilles Kahn was one of the most influential figures in the development of computer science and information technology, not only in Europe but throughout the world. This volume of articles by several leading computer scientists serves as a fitting memorial to Kahn’s achievements and reflects the broad range of subjects to which he contributed through his scientific research and his work at INRIA, the French National Institute for Research in Computer Science and Control. The editors also reflect upon the future of computing: how it will develop as a subject in itself and how it will affect other disciplines, from biology and medical informatics, to web and networks in general. Its breadth of coverage, topicality, originality and depth of contribution, make this book a stimulating read for all those interested in the future development of information technology.

[10] A. E. Ashcroft and W. W. Wadge . Lucid, the Dataflow Programming Language. Number 22 in APIC Studies in Data Processing. Academic Press, 1985.
[10] A. V. Bakre and B. R. Badrinath , Implementation and performance evaluation of Indirect TCP. IEEE Transactions on Computers, 46(3):260–278, 1997.
[10] C. Fournet and G. Gonthier . The reflexive CHAM and the join-calculus. In Proceedings of the 23rd ACM Symposium on Principles of Programming Languages, pp. 372–385. ACM Press, 1996.
[10] C. Gunter and D. Scott , Semantic domains. In: J. Van Leeuwen (ed.), Handbook of Theoretical Computer Science, Volume B, pp. 633–674. Elsevier, 1990.
[10] C. Pair , Concerning the syntax of Algol 68, Algol Bulletin 31:16–27, 1970.
[10] C. Paulin-Mohring and B. Werner . Synthesis of ML programs in the system Coq. Journal of Symbolic Computation 15:607–640, 1993.
[10] H. Kokko , M. D. Jennions and R. Brooks . Unifying and testing models of sexual selection. Annual Reviews of Ecology, Evolution and Systematics, 37:43–66, 2006.
[10] J. B. Dennis . First Version Data Flow Procedure Language. Technical Report MAC TM61, MIT Laboratory for Computer Science, 1974.
[10] J. Harrison . The HOL light theorem prover. www.cl.cam.ac.uk/∼jrh13/hol–light/, 2006.
[10] L. Hascoët and M. Araya-Polo . The adjoint data-flow analyses: Formalization, properties, and applications. In [1], pp. 135–146. 2006.
[10] N. Halbwachs , P. Caspi , P. Raymond and D. Pilaud . The synchronous dataflow programming language lustre. Proceedings of the IEEE, 79(9):1305–1320, 1991.
[10] O. Clatz , M. Sermesant , P.-Y. Bondiau , et al. Realistic simulation of the 3D growth of brain tumors in MR images coupling diffusion with mass effect. IEEE Transactions on Medical Imaging, 24(10):1334–1346, 2005.
[10] P. Borras , D. Clément , T. Despeyroux , J. Incerpi , G. Kahn , B. Lang and V. Pascual . Centaur: the system. In Third Symposium on Software Development Environments, 1988.
[10] P.-L. Curien , Symmetry and interactivity in programming, Bulletin of Symbolic Logic 9(2):169–180 (2003).
[10] R. D. King , K. E. Whelan , F. M. Jones , et al. Functional genomic hypothesis generation and experimentation by a robot scientist. Nature 427:247–252, 2004.
[10] R. Hindley . Basic Simple Type Theory. Cambridge University Press, 1997.
[10] S. Horwitz , J. Prins and T. Reps . On the adequacy of program dependence graphs for representing programs. In POPL, pp. 146–157, 1988.
[10] T. Nipkow and L. C. Paulson . Proof pearl: Defining functions over finite sets. In J. Hurd (ed.) Theorem Proving in Higher Order Logics (TPHOLs 2005), volume 3603, Lecture Notes in Computer Science, pp. 385–396. Springer-Verlag, 2005.
[10] Y. Bertot . Occurrences in debugger specifications. In PLDI '91: Proceedings of the ACM SIGPLAN 1991 Conference on Programming Language Design and Implementation, pp. 327–337, New York, NY, USA, 1991. ACM Press.
[10] Y. Coscoy , G. Kahn and L. Thery . Extracting text from proofs. In M. Dezani-Ciancaglini and G. Plotkin (eds) Proc. Second International Conference on Typed Lambda Calculi and Applications, volume 902 Lecture Notes in Computer Science, pp. 109–123, Springer-Verlag, 1995.
[11] A. M. Pitts . Nominal logic, A first order theory of names and binding. Information and Computation, 186:165–193, 2003.
[11] C. A. R. Hoare . Communicating sequential processes. Communications of the ACM, 21(8):666–677, 1978.
[11] D. Scott , Outline of a Mathematical Theory of Computation. Oxford Monograph PRG-2. Oxford University, 1970.
[11] G. Huet , Résolution d'équations dans des langages d'ordre 1, 2, …, ω. Doctoral dissertation, Université Paris 7, 1976.
[11] G. Huet and G. Plotkin (eds) Logical Frameworks: First International Workshop on Logical Frameworks, Antibes, May, 1990. Cambridge University Press, 1991.
[11] G. Huet and J.-J. Lévy . Computations in orthogonal rewriting systems I and II, In Computational Logic; Essays in Honor of Alan Robinson. pp. 395–443. The MIT Press, 1991.
[11] G. Kahn . The semantics of a simple language for parallel programming. In Information Processing 74. North-Holland, 1974.
[11] H. B. Curry . Some logical aspects of grammatical structure. In Roman Jakobson , editor, Structure of Language and its Mathematical Aspects: Proceedings of the Twelfth Symposium in Applied Mathematics, pp. 56–68. American Mathematical Society, 1963.
[11] H. Balakrishnan , V. Padmanabhan , S. Seshan and R. Katz . A comparison of mechanisms for improving TCP performance over wireless links. IEEE/ACM Transactions on Networking, 5(6), 1997.
[11] H. Kobayashi , M. Kaern , M. Araki , et al. Programmable cells: interfacing natural and engineered gene networks. Proc. Nat. Acad. Sci., USA, 101(22):8414–8419, 2004.
[11] J. L. Baer . A survey of some theoretical aspects of multiprocessing. ACM Comput. Surv., 5(1):31–80, 1973.
[11] J. M. McNamara , et al. A dynamic game-theoretic model of parental care. Journal of Theoretical Biology 205:605–623, 2000.
[11] J.-Y. Girard , Linear logic, Theoretical Computer Sciences 50:1–102 (1987).
[11] L. Hascoët , U. Naumann and V. Pascual . To-be-recorded analysis in reverse mode Automatic Differentiation. Future Generation Computer System, 21(8):1401–1417, 2005.
[11] M. Geilen and T. Basten . Requirements on the execution of Kahn process networks. In European Symposium on Programming Languages and Systems, Lecture Notes in Computer Science, pp. 319–334, Springer, 2003.
[11] O. Commowick , R. Stefanescu , P. Fillard , et al. Incorporating statistical measures of anatomical variability in atlas-to-subject registration for conformal brain radiotherapy. In J. Duncan and G. Gerig (eds) Proceedings of the 8th International Conference on Medical Image Computing and Computer Assisted Intervention – MICCAI 2005, Part II, Palm Springs, CA, USA, October 26–29, 2005. volume 3750, Lecture Notes in Computer Science, pp. 927–934, Springer-Verlag, 2005.
[11] S. Boutin . Using reflection to build efficient and certified decision procedures. In Theoretical Aspects of Computer Science, volume 1281, Lecture Notes in Computer Science, pp. 515–529. Springer-Verlag, 1997.
[11] S. Horwitz , J. Prins and T. Reps . Integrating non-interfering versions of programs. TOPLAS, 11(3):345–387, 1989.
[11] Y. Bertot . Origin functions in lambda-calculus and term rewriting systems. In J.-C. Raoult (ed.), CAAP, volume 581, Lecture Notes in Computer Science, pp. 49–65. Springer, 1992.
[12] A. Chaieb . Proof-producing program analysis. In K. Barkaoui , A. Cavalcanti and A. Cerone (eds) ICTAC, volume 4281, Lecture Notes in Computer Science, pp. 287–301. Springer-Verlag, 2006.
[12] A. M. Pitts and M. J. Gabbay . A metalanguage for programming with bound names modulo renaming. In Proc. of the 5th International Conference on Mathematics of Program Construction (MPC), volume 1837, Lecture Notes in Computer Science, pp. 230–255. Springer-Verlag, 2000.
[12] C.-J. Hsu , F. Keceli , M.-Y. Ko , S. Shahparnia and S. S. Bhattacharyya . DIF: An interchange format for dataflow-based design tools. In International Workshop on Systems, Architectures, Modeling, and Simulation, Samos, Greece, July 2004.
[12] F. Brichet , J. Roberts , A. Simonian and D. Veitch . Heavy traffic analysis of a storage model with long range dependent on/off sources. Queueing Systems, 23, 1996.
[12] G. Berry and P.-L. Currien . Sequential algorithms on concrete data structures. Theoret. Comput. Sci., 20:265–322, 1982.
[12] G. Huet and G. Plotkin (eds) Logical Environments: Second International Workshop on Logical Frameworks, Edinburgh, May, 1991. Cambridge University Press, 1993.
[12] G. Kahn . The semantics of a simple language for parallel programming. Information Processing, 74:471–475, 1974.
[12] G. Kahn . The semantics of simple language for parallel programming. In IFIP Congress, pp. 471–475, 1974.
[12] G. Kahn and D. MacQueen . Coroutines and networks of parallel processes. In B. Gilchrist (ed.) Information Processing 77. North-Holland, 1977.
[12] J. Vuillemin , Proof Techniques for Recursive Programs. PhD thesis, Stanford Computer Science Department. 1973.
[12] J.-J. Rousseau . Discours sur l'origine et les fondemens de l'inégalité parmi les hommes (Deuxième partie), Dijon, 1755. (See http://hypo.ge.ch/athena/rousseau/jjr_ineg.html)
[12] J.-W. Klop . Combinatory Reduction Systems. PhD thesis. Mathematical Centre Tracts 127, CWI, Amsterdam, 1980.
[12] J.-Y. Girard , Locus Solum, Mathematical Structures in Computer Science (2001).
[12] L. Hascoët and V Pascual . Tapenade 2.1 user's guide. Technical report 300, INRIA, 2004.
[12] P. Mosses , Denotational semantics. In: J. Van Leeuwen (ed.), Handbook of Theoretical Computer Science, Volume B, pp. 575–632. Elsevier, 1990.
[12] Ph. de Groote . Towards abstract categorial grammars. In Association for Computational Linguistics, 39th Annual Meeting and 10th Conference of the European Chapter, Toulouse, France, pp. 148–155, 2001.
[12] S. Basu , R. Mehreja , S. Thiberge , M.-T. Chen and R. Weiss . Spatiotemporal control of gene expression with pulse generating networks. Proc. Nat. Acad. Sci., USA 101(17):6355–6360, 2004.
[12] S. Cotin , H. Delingette and N. Ayache . A hybrid elastic model allowing real-time cutting, deformations and force-feedback for surgery training and simulation. The Visual Computer, 16(8):437–452, 2000.
[12] Y. Bertot , G. Kahn and L. Théry . Proof by pointing. In M. Hagiya and J. C. Mitchell (eds), TACS, volume 789 Lecture Notes in Computer Science, pp. 141–160. Springer, 1994.
[13] A. El Dada . Implementation of the Arabic numerals and their syntax in GF. In Computational Approaches to Semitic Languages: Common Issues and Resources, ACL-2007 Workshop, June 28, 2007, Prague, 2007.
[13] A. Jantsch and I. Sander . Models of computation and languages for embedded system design. IEE Proceedings on Computers and Digital Techniques, 152(2):114–129, 2005.
[13] D. Kuck , R. Kuhn , B. Leasure , D. Padua and M. Wolfe . Dependence graphs and compiler optimizations. In POPL, pp. 207–218, 1981.
[13] G. Berry and P.-L. Currien . The kernel of the applicative language cds: theory and practice. In Proc. French-US Seminar on the Applications of Algebra to Language Definition and Compilation, pp. 35–87. Cambridge University Press, 1985.
[13] G. Kahn and D. MacQueen , Coroutines and networks of parallel processes. In Proc. IFIP 1977, B. Gilchrist (ed.), North-Holland, pp. 993–998 (1977).
[13] G. Kahn and G. D. Plotkin . Concrete domains. Theoretical Computer Science, 121(1& 2):187–277, 1993.
[13] Isabelle Homepage . www.cl.cam.ac.uk/Research/HVG/Isabelle/, 2003.
[13] J. G. Csernansky , L. Wang , S. C. Joshi , J. T. Ratnanather and M. I. Miller . Computational anatomy and neuropsy chiatric disease: probabilistic assessment of variation and statistical inference of group difference, hemispheric asymmetry and time-dependent change. NeuroImage, 23(Supplement 1):S56–S68, 2004. Special Issue: Mathematics in Brain Imaging.
[13] L. Samuelson . Evolutionary Games and Equilibrium Selection. MIT Press, 1998.
[13] M. Rabin , Decidability of second-order theories and automata on infinite trees, Transactions of the American Mathematical Society, 141:1–35, 1969.
[13] M. Tofte . Operational Semantics and Polymorphic Type Inference. PhD thesis. Edinburgh University, 1988.
[13] P. Embrechts , C. Kluppelberg and T. Mikosch Modelling Extremal Events. Springer, 1997.
[13] P. Landin . A correspondence between Algol 60 and Church's lambda-notation. CACM, 8(2):89–101, 1965.
[13] R. Constable , S. F. Allen , H. M. Bromley , W. R. Cleaveland , J. F. Cremer , R. W. Harber , D. J. Howe , T. B. Knoblock , N. P. Mendler , P. Panangaden , J. T. Sasaki and S.F. Smith . Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, 1986.
[13] R. Milner . A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer-Verlag, 1980.
[13] S. Billot and B. Lang . The structure of shared forests in ambiguous parsing. In ACL, pp. 143–151, 1989.
[13] U. Naumann . Optimal accumulation of Jacobian matrices by elimination methods on the dual computational graph. Mathematical Programming, Series A, 99(3):399–421, 2004.
[14] A. El Dada and A. Ranta . Implementing an open source arabic resource grammar in GF. In M. A. Mughazy (ed.) Perspectives on Arabic Linguistics XX, pp. 209–232. John Benjamins, Amsterdam and Philadelphia, 2007.
[14] C. Coquand . Agda. www.cs.chalmers.se/∼catarina/agda.
[14] C. Laneve . Distributive evaluations of lambda-calculus. Fundamenta Informaticae, 20(4):333–352, 1994.
[14] C. Urban and S. Berghofer . A recursion combinator for nominal datatypes implemented in Isabelle/HOL. In Proc. of the 3rd International Joint Conference on Automated Reasoning (IJCAR), volume 4130, Lecture Notes in Artificial Intelligence, pp. 498–512. Springer-Verlag, 2006.
[14] D. E. Knuth . Literate Programming. CSLI, 1992.
[14] D. Kuck , Y. Muraoka , and S. Chen . On the number of operations simultaneously executable in FORTRAN-like programs and their resulting speed-up. IEEE Trans. on Computers, C-21(12):1293–1310, 1972.
[14] D. Pilaud , P. Caspi , N. Halbwachs and J. Plaice . Lustre: a declarative language for programming synchronous systems. In 14th ACM Conference on Principles of Programming Languages, pp. 178–188, Munich, January 1987.
[14] G. Kahn and G. Plotkin , Concrete domains, Theoretical Computer Science 12:187–277 (1993).
[14] G. Sénizergues , Complete formal systems for equivalence problems, Theoretical Computer Science, 231:309–334, 1999.
[14] H. Delingette , X. Pennec , L. Soler , J. Marescaux and N. Ayache . Computational models for image guided, robot-assisted and simulated medical interventions. Proceedings of the IEEE, 94(9):1678–1688, 2006.
[14] P. Borras , D. Clément , Th. Despeyroux , J. Incerpi , G. Kahn , B. Lang and V. Pascual . CENTAUR: The system. In Software Development Environments (SDE), pp. 14–24, 1988.
[14] S. Brookes and S. Geva . Continuous functions and parallel algorithms on concrete data structures. In Proc. 7th International Conf. on Mathematical Foundations of Programming Semantics, volume 598 in Lecture Notes in Computer Science, 1991.
[14] S. Foss and S. Zachary , The maximum on a random time interval of a random walk with long-tailed increments and negative drift. Annals of Applied Probability, 13(1):37–53, 2003.
[14] T. Murata . Petri nets: Properties, analysis and applications. Proceedings of the IEEE, 77(4):541–580, 1989.
[14] U. Naumann . Optimal Jacobian accumulation is NP-complete. Mathematical Programing, 2006. in press. Appeared online first.
[14] W. H. Sandholm . Population Games and Evolutionary Dynamics. Preprint, http://www.ssc.edu/∼whs/book/index.html, 2007.
[14] W. M. Johnston , J. R.P. Hanna and R. J. Millar . Advances in dataflow programming languages. ACM Computing Surveys, 36(1):1–34, 2004.
[15] C. Urban , S. Berghofer and M. Norrish . Barendregt's variable convention in rule inductions. In Proc. of the 21th International Conference on Automated Deduction (CADE), volume 4603, Lecture Notes in Artificial Intelligence, pp. 35–50. Springer-Verlag, 2007.
[15] G. Kahn . The semantics of a simple language for parallel programming. In Proc. of the IFIP Congress 74. North-Holland Publishing Co., 1974.
[15] G. Sénizergues , L(A) = L(B)?, Theoretical Computer Science, 251:1–166, 2001.
[15] H. R. Barradas . Une approche à la dérivation formelle de systèmes en Gamma. PhD thesis, Université de Rennes 1, France, 1993.
[15] I. L. Dryden and K. V. Mardia . Statistical Shape Analysis. John Wiley and Sons, 1998.
[15] J. G. Wardrop . Some theoretical aspects of road trafic. Proceedings of the Institution of Civil Engineers, Part II, 1:325–378, 1952.
[15] J. Laird , Bistability: an extensional characterization of sequentiality. In Proc. Computer Science and Logic 2003, Lecture Notes in Computer Science 2803, Springer-Verlag (2003).
[15] J.-J. Lévy . An algebraic interpretation of the λβ-calculus and a labeled λ-calculus. In C. Böhm (ed.), Lambda-Calculus and Computer Science Theory, volume 37 of Lecture Notes in Computer Science, pp. 147–165. Springer, March 1975.
[15] K. Ottenstein , R. Ballance and A. MacCabe . The program dependence web: A representation supporting control-, data-, and demand-driven interpretation of imperative languages. In PLDI, pp. 257–271, 1990.
[15] L. Magnusson and B. Nordström . The ALF proof editor and its proof engine. In Types for Proofs and Programs, volume 806, Lecture Notes in Computer Science, pp. 213–237, Nijmegen, 1994. Springer-Verlag.
[15] M. Forsberg and A. Ranta . Functional Morphology. In ICFP 2004, Showbird, Utah, pp. 213–223, 2004.
[15] M. G. J. van den Brand , M. Bruntink , G. R. Economopoulos , H. A. de Jong , P. Klint , T. Kooiker , T. van der Storm and J.J. Vinju . Using the meta-environment for maintenance and renovation. In Proceedings of the 11th European Conference on Software Maintenance and Reengineering (CSMR'07), pp. 331–332. IEEE Computer Society, March 21–23 2007.
[15] P. Cousot and R. Cousot . Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the Fourth Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, pp. 238–252, Los Angeles, California, 1977. ACM Press, New York, NY.
[15] R. B. Jain and T. Ott . Design and Implementation of split TCP in the Linux Kernel. Proceedings of the Globecom, San Francisco, November 2006.
[15] S. Brookes . Historical introduction to “concrete domains” by G. Kahn and G. D. Plotkin. Theoret. Comput. Sci., 121(1–2):179–186, 1993.
[15] U. Naumann , J. Utke , A. Lyons and M. Fagan . Control flow reversal for adjoint code generation. In Proceedings of the Fourth IEEE International Workshop on Source Code Analysis and Manipulation (SCAM 2004), pp. 55–64. IEEE Computer Society, 2004.
[16] C. Urban and C. Tasson . Nominal Techniques in Isabelle/HOL. In Proc. of the 20th International Conference on Automated Deduction (CADE), volume 3632, Lecture Notes in Computer Science, pp. 38–53, Springer-Verlag, 2005.
[16] E. W. Dijkstra . A discipline of Programming. Prentice Hall, 1976.
[16] G. Kahn and D. B. MacQueen . Coroutines and networks of parallel processes. In B. Gilchrist (ed.), Information Processing, pages 993–998. North-Holland Publishing Co., 1977.
[16] I. Walukiewicz , Completeness of Kozen's axiomatization of propositional µ-calculus, Information and Computation, 157:142–182, 2000.
[16] J. Duncan and N. Ayache . Medical image analysis: Progress over two decades and the challenges ahead. IEEE Transactions on Pattern Analysis and Machine Intelligence, 22(1):85–106, 2000.
[16] J. Laird , Locally boolean domains, Theoretical Computer Science 342:132–248 (2005).
[16] J. Nocedal and S.-J. Wright . Numerical Optimization. Springer, Series in Operations Research, 1999.
[16] J.-J. Lévy . Réductions correctes et optimales dans le lambda calcul. PhD thesis, University of Paris 7, 1978. (in French).
[16] K. Ottenstein and L. Ottenstein . The program dependence graph in a software development environment. In Softw. Eng. Symp. on Practical Softw. Dev. Environments, pp. 177–184, 1984.
[16] M. G. J. van den Brand , A. van Deursen , J. Heering , H. A. de Jong , M. de Jonge , T. Kuipers , P. Klint , L. Moonen , P.A. Olivier , J. Scheerder , J. J. Vinju , E. Visser and J. Visser . The ASF+SDF Meta-Environment: a component-based language development environment. In R. Wilhelm (ed.), Compiler Construction (CC '01), volume 2027, Lecture Notes in Computer Science, pp. 365–370. Springer-Verlag, 2001.
[16] M. Karaliopoulos , R. Tafazolli and B. Evans . Modeling split-TCP latency and buffering requirements in GEO satellite networks. Proceeding of the IEEE Wireless Communications and Networking Conference, vol. 3, pp. 1509–1514, March 2005.
[16] P. Martin-Löf . Intuitionistic Type Theory. Bibliopolis, Napoli, 1984.
[16] T. Hallgren and A. Ranta . An extensible proof text editor. In M. Parigot and A. Voronkov (eds) LPAR-2000, volume 1955 LNCS/LNAI, pp. 70–84. Springer, 2000.
[16] T. Winquist and R. E. Lemon . Sexual selection and exaggerated male tail length in birds. The American Naturalist, 143:95–116, 1994.
[16] W. H. Burge . Recursive Programming Techniques. Addison Wesley, 1975.
[17] A. Zahavi . Mate selection – a selection for the handicap. Journal of Theoretical Biology, 53:205–214, 1975.
[17] B. Nordström , K. Petersson and J. M. Smith . Martin-Löf's Type Theory, chapter 1, pp. 1–33. Oxford University Press, 2001.
[17] D. Lazaro Cuadrado , A.P. Ravn and P. Koch . Automated distributed simulation in Ptolemy II. In Parallel and Distributed Computing and Networks (PDCN). Acta Press, 2007.
[17] F. Lamarche , Sequentiality, games and linear logic. In Proc. CLICS Workshop, Aarhus University, DAIMI-397-II (1992).
[17] G. Dowek , A. Felty , H. Herbelin , G. Huet , C. Murthy , C. Parent , C. Paulin-Mohring and B. Werner . The Coq Proof Assistant User's Guide. INRIA, May 1993. Version 5.8.
[17] G. Huet . A functional toolkit for morphological and phonological processing, application to a Sanskrit tagger. Journal of Functional Programming, 15(4):573–614, 2005.
[17] J. Utke , A. Lyons and U. Naumann . Efficient reversal of the intraprocedural flow of control in adjoint computations. J. Syst. Softw., 79(9):1280–1294, 2006.
[17] J.-J. Lévy . Optimal reductions in the lambda-calculus. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 159–191. Academic Press, 1980.
[17] K. Pingali , M. Beck , R. Johnson , M. Moudgill , and P. Stodghill . Dependence flow graphs: An algebraic approach to program dependencies. In Advances in Languages and Compilers for Parallel Processing, pp. 445–467. M.I.T. Press, 1991.
[17] M. G. J. van den Brand , H. A. de Jong , P. Klint and P. Olivier . Efficient Annotated Terms. Software, Practice & Experience, 30:259–291, 2000.
[17] P. Fillard , V. Arsigny , X. Pennec , K. M. Hayashi , P. M. Thompson and N. Ayache . Measuring brain variability by extrapolating sparse tensor fields measured on sulcal lines. Neuroimage, 34(2):639–650, 2007. Also as INRIA Research Report 5887, April 2006.
[17] U. Keller and G. Biersack . A congestion control model for multicast overlay networks and its performance. Proceedings of the Networked Group Communication, Boston, MA, 2002.
[17] W. H. Burge . Stream processing functions. IBM J. Res. Develop., pp. 12–25, 1975.
[18] C. Forest , H. Delingette and N. Ayache . Removing tetrahedra from manifold tetrahedralisation: application to real-time surgical simulation. Medical Image Analysis, 9(2):113–122, 2005.
[18] E. A. Lee and T. M. Parks . Dataflow process networks. Proceedings of the IEEE, 83(5):773–801, 1995.
[18] G. Ramalingam and T. Reps . Appendix A: Proofs. “www.cs.wisc.edu/wpis/papers/soprgs08-proofs.pdf”.
[18] J. Utke , U. Naumann , M. Fagan , et al. Open AD/F: A Modular, Open-source Tool for Automatic Differentiation of Fortran codes. Technical report ANL/MCS-P1230-0205, Argonne National Laboratory, 2006. Submitted to ACM TOMS.
[18] J.-C. Filliâtre . Proof of imperative programs in type theory. In International Workshop TYPES'98, volume 1657, Lecture Notes in Computer Science, pp. 78–92. Springer-Verlag, March 1998.
[18] L. Maranget . La stratégie paresseuse. PhD thesis, University of Paris 7, July 1992.
[18] L. Padovani and R. Solmi . An investigation on the dynamics of direct-manipulation editors for mathematics. In Asperti et al. [2], pp. 302–316.
[18] M. G. J. van den Brand and P. Klint . ATerms for manipulation and exchange of structured data: It's all about sharing. Information and Software Technology, 49(1):55–64, 2007.
[18] M. Humayoun . Urdu Morphology, Orthography and Lexicon Extraction. MSc Thesis, Department of Computing Science, Chalmers University of Technology, 2006.
[18] R. M. Burstall . Design considerations for a functional programming language. In Infotech State of the Art Conference: The Software Revolution, Copenhagen, October 1977.
[18] S. Kopparty , S. V. Krishnamurthy , M. Faloutsos and S. Tripathi . split TCP for mobile ad hoc networks. Proceedings of IEEE Globecom '02, Taipei, November 2002.
[18] T. Loew , Locally Boolean Domains and Universal Models for Infinitary Sequential Languages, PhD Thesis, Technische Universität Darmstadt (2006).
[19] C. Fouard , G. Malandain , S. Prohaska and M. Westerhoff . Blockwise processing applied to brain microvascular network study. IEEE Transactions on Medical Imaging, 25(10):1319–1328, 2006.
[19] G. Kwon and J. Byers . ROMA: reliable overlay multicast with loosely coupled TCP connections. Proceedings of the IEEE Infocom, February 2004.
[19] G. Ramalingam and T. Reps . Semantics of program representation graphs. TR-900, Computer Science Department, University of Wisconsin, Madison, WI, 1989.
[19] J. Khegai . GF parallel resource grammars and Russian. In Coling/ACL 2006, pp. 475–482, 2006.
[19] M. G. J. van den Brand , A. T. Kooiker , J. J. Vinju and N.P. Veerman . A Language Independent Framework for Context-sensitive Formatting. In 10th Conference on Software Maintenance and Reengineering (CSMR 2006), pp. 631–634. IEEE Computer Society Press, 2006.
[19] M. J. C. Gordon and T. F. Melham . Introduction to HOL : a theorem-proving environment for higher-order logic. Cambridge University Press, 1993.
[19] P.-A. Melliès . A factorisation theorem in rewriting theory. In Proceedings of the 7th Conference on Category Theory and Computer Science, volume 1290, Lecture Notes in Computer Science, pp. 49–68, Santa Margherita Ligure. Springer, 1997.
[19] R. M. Burstall , J. S. Collins , and R. J. Popplestone . Programming in POP-2. Edinburgh University Press, 1977.
[19] R. Pollack . The LEGO proof assistant. www.dcs.ed.ac.uk/home/lego/, 1997.
[19] T. Streicher , Laird domains, draft (2002).
[19] Y. Lin , R. Mullenix , M. Woh , S. Mahlke , T. Mudge , A. Reid and K. Flautner . SPEX: A programming language for software defined radio. In Software Defined Radio Technical Conference and Product Exposition, Orlando, 2006.
[1] A. Aho , R. Sethi and J. Ullman . Compilers: Principles, Techniques and Tools. Addison-Wesley, 1985.
[1] A. Appel . Modern Compiler Implementation in Java. Cambridge University Press, 1998.
[1] Agda homepage . unit.aist.go.jp/cvs/Agda/.
[1] Arvind , L. Bic and T. Ungerer . Evolution of data-flow computers. In J.-L. Gaudiot and L. Bic (eds), Advanced Topics in Data-Flow Computing. Prentice-Hall, 1991.
[1] B. Courcelle and J. Vuillemin , Completeness results for the equivalence of recursive schemes, Journal of Computer System Science 12:179–197, 1976.
[1] B. E. Aydemir , A. Bohannon , M. Fairbairn , J. N. Foster , B. C. Pierce , P. Sewell , D. Vytiniotis , G. Washburn , S. Weirich and S. Zdancewic . Mechanized metatheory for the masses: The POPLmark challenge. In Proceedings of the Eighteenth International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2005), pp. 50–65. Springer-Verlag, 2005.
[1] C. J. Bampfylde and M. A. Lewis . Biological control through intraguild predation: case studies in pest control, invasive species and range expansion. Bulletin of Mathematical Biology 69:1031–1066, 2007.
[1] D. Clément , J. Despeyroux , T. Despeyroux , L. Hascoet and G. Kahn . Natural semantics on the computer. In K. Fuchi and M. Nivat (eds), Proceedings of the France-Japan AI and CS Symposium, ICOT, Japan, pp. 49–89, 1986. Also Technical Memorandum PL-86-6 Information Processing Society of Japan and Rapport de recherche #0416, INRIA.
[1] Debugging advice can be found at http://www.wikihow.com/Debug-a-Tamagotchi.
[1] E. Altman , K. Avrachenkov , C. Barakat and R. Nunez-Queija . Statedependent M/G/1 type queueing analysis for congestion control in data networks. Computer Networks, 39(6), 789–808, 2002.
[1] F. Cardone and M. Coppo , Decidability properties of recursive types. ICTCS 2003, Bertinoro, Italy, Lecture Notes in Computer Science 2841, pp. 242–255, Springer-Verlag, 2003.
[1] H. Abelson , G. J. Sussman , and J. Sussman . Structure and Interpretation of Computer Programs. McGraw-Hill, New York, 1985.
[1] I. Attali . A natural semantics for Eiffel dynamic binding. ACM Transactions on Programming Languages and Systems (TOPLAS), 18(5), 1996.
[1] J.-P. Banâtre , P. Fradet , J.-L. Giavitto and O. Michel (eds). Unconventional Programming Paradigms (UPP'04), volume 3566 of Lecture Notes in Computer Science, Revised Selected and Invited Papers of the International Workshop, 2005. Springer-Verlag.
[1] M. Bücker , G. Corliss , P. Hovland , U. Naumann and B. Norris (eds). Automatic Differentiation: Applications, Theory, and Implementations. LNCSE. Springer, 2006. Selected papers from AD2004, Chicago, July 2004.
[1] P. Audebaud and C. Paulin-Mohring . Proofs of randomized algorithms in Coq. In T. Uustalu (ed.) Mathematics of Program Construction, MPC 2006, volume 4014, Lecture Notes in Computer Science, Kuressaare, Estonia, July 2006. Springer-Verlag, 2006.
[1] R. Amadio and P.-L. Curien , Domains and Lambda-calculi, Cambridge University Press (1998).
[1] R. Amadio and P.-L. Curien. Domains and Lambda-calculi. Cambridge University Press, 1998.
[1] S. Emmott (ed.). Towards 2020 Science, available from http://www.research.microsoft.com/towards2020science.
[1] V. Arsigny , P. Fillard , X. Pennec and N. Ayache . Log-euclidean metrics for fast and simple calculus on diffusion tensors. Magnetic Resonance in Medicine, 56(2):411–421, 2006. PMID: 16788917.
[1] Y. Bertot and P. Casteran . Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series 2004, XXV, 469 pp.
[20] A. Ranta . Grammatical Framework Homepage. www.cs.chalmers.se/∼aarne/GF/, 1999–2005.
[20] M. G. J. van den Brand , A. Sellink and C. Verhoef . Control flow normalization for COBOL/CICS legacy system. In CSMR, pp. 11–20. IEEE Computer Society, 1998.
[20] M. J. C. Gordon , R. Milner and C. P. Wadsworth . Edinburgh LCF, volume 78, Lecture Notes in Computer Science. Springer-Verlag, 1979.
[20] M. Luglio , M. Y. Sanadidi , M. Gerla and J. Stepanek . On-board satellite “split TCP” proxy. IEEE JSAC, 22(2), 2004.
[20] N. C. Fox and J. M. Schott . Imaging cerebral atrophy: normal ageing to Alzheimer's disease. Lancet, 363(9406), 2004.
[20] P. Martin-Löf . Constructive mathematics and computer programming. In Cohen, Los, Pfeiffer and Podewski (eds) Logic, Methodology and Philosophy of Science VI, pp. 153–175. North-Holland, Amsterdam, 1982.
[20] R. M. Burstall and J. Darlington . A tranformation system for developing recursive programs. J. ACM, 24(1), 1977.
[20] R. Nederpelt , J. Geuvers and R. d. Vrijer . Selected Papers on Automath, volume 133, Studies in Logic and the Foundations of Mathematics. North-Holland, 1994.
[20] S. G. Matthews . An extensional treatment of lazy data flow deadlock. Theoretical Computer Science, 151(1):195–205, 1995.
[20] T. Reps and W. Yang . The semantics of program slicing and program integration. In CCIPL, pp. 360–374, 1989.
[21] A. G. Olson and B. L. Evans . Deadlock detection for distributed process networks. In ICASSP, 2005.
[21] A. Ranta . Grammatical Framework: A Type-Theoretical Grammar Formalism. Journal of Functional Programming, 14(2):145–189, 2004.
[21] B. Rosen , M. Wegman , and F. Zadeck . Global value numbers and redundant computations. In POPL, pp. 12–27, 1988.
[21] C. A. R. Hoare . An axiomatic basis for computer programming. Communications of the ACM, 12:576–580, 1969.
[21] L. France , A. Angelidis , P. Meseure , et al. Implicit representations of the human intestines for surgery simulation. In M. Thiriet (ed.) Conference on Modelling and Simulation for Computer-aided Medicine and Surgery (MS4CMS'02), volume 12, European Series in Applied and Industrial Mathematics, pp. 1–7, 2002.
[21] M. G. J. van den Brand and E. Visser . Generation of formatters for context-free languages. ACM Transactions on Programming Languages and Systems, 5(1):1–41, 1996.
[21] R. M. Burstall , D. B. MacQueen , and D. Sannella . Hope: An experimental applicative language. In Conference Record of the 1980 Lisp Conference, pp. 136–143, August 1980. Stanford.
[21] R. Montague . Formal Philosophy. Yale University Press, New Haven, 1974. Collected papers edited by R. Thomason.
[21] T. Liggett , An improved subadditive ergodic theorem. Annals of Probability, 13:1279–1285, 1985.
[21] V. V. Oostrom and R. D. Vrijer . Equivalence of reductions. In Terese, Term Rewriting Systems. Cambridge University Press, March 2003.
[22] A. F. Frangi , W. J. Niessen and M. A. Viergever . Three-dimensional modeling for functional analysis of cardiac images: a review. IEEE Transactions on Medical Imaging, 20(1):2–25, 2001.
[22] Centaur web pp. , Last visit December 2006. http://www-sop.inria.fr/croap/centaur/centaur.html.
[22] G. Kahn . Natural semantics. In K. Fuchi and M. Nivat (eds) Programming of Future Generation Computers, pp. 237–258. North-Holland, 1988. (also appears as INRIA Report no. 601).
[22] G. Plotkin . Call-by-name, call-by-value, and the lambda-calculus. Theoretical Computer Science, 1, 1975.
[22] O. M. G. (OMG) . A UML profile for MARTE, beta 1. OMG Adopted Specification ptc/07–08–04, August 2007.
[22] P. Caspi , D. Pilaud , N. Halbwachs and J. A. Plaice . LUSTRE: a declarative language for real-time programming. In POPL '87: Proceedings of the 14th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 178–188, New York, NY, USA, 1987. ACM Press.
[22] R. Muskens . Lambda grammars and the syntax-semantics interface. In R. van Rooy and M. Stokhof (eds) Proceedings of the Thirteenth Amsterdam Colloquium, pp. 150–155, Amsterdam, 2001.
[22] R. Selke . A rewriting semantics for program dependence graphs. In POPL, pp. 12–24, 1989.
[22] The Types Project Homepage . www.cs.chalmers.se/Cs/Research/Logic/Types/.
[22] V. Misra , W.-B. Gong and D. Towsley , Stochastic differential equation modeling and analysis of TCP-windowsize behavior. In Performance'99, Istanbul (Turkey), October 1999
[23] C. Germain , V. Breton , P. Clarysse , et al. Grid-enabling medical image analysis. Journal of Clinical Monitoring and Computing, 19(4–5):339–349, 2005. PMID: 16328948.
[23] D. van Daalen . The Language Theory of Automath. PhD thesis, TUE, 1980.
[23] I. Norros , A storage model with self-similar input, Queueing Systems, 16:387–396, 1994.
[23] J. Chailloux , M. Devin , F. Dupont , J.-M. Hullot , B. Serpette and J. Vuillemin . Le_Lisp version 15.2, le manuel de réference. Technical report, INRIA, 1986.
[23] L. Théry , Y. Bertot and G. Kahn . Real theorem provers deserve real user-interfaces. In Proceedings of the Fifth ACM SIGSOFT Symposium on Software Development Environments, pp. 120–129, 1992.
[23] N. Perera and A. Ranta . Dialogue System Localization with the GF Resource Grammar Library. In SPEECHGRAM 2007: ACL Workshop on Grammar-Based Approaches to Spoken Language Processing, June 29, 2007, Prague, 2007.
[23] P. Caspi and M. Pouzet . Synchronous Kahn networks. In ICFP '96: Proceedings of the first ACM SIGPLAN International Conference on Functional Programming, pp. 226–238, New York, NY, USA, 1996. ACM Press.
[23] P. Letouzey . A new extraction for Coq. In H. Geuvers and F. Wiedijk (eds) TYPES 2002, volume 2646, Lecture Notes in Computer Science, pp. 200–219. Springer-Verlag, 2003.
[23] R. Shapiro and H. Saint . The representation of algorithms. Tech. Rep. CA-7002-1432, Massachusetts Computer Associates, 1970.
[23] T. M. Parks . Bounded Scheduling of Process Networks. PhD, UC Berkeley, 1995.
[24] A. Cohen , M. Duranton , C. Eisenbeis , C. Pagetti , F. Plateau and M. Pouzet . N-synchronous Kahn networks: a relaxed model of synchrony for real-time systems. In POPL '06: Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 180–193, New York, NY, USA, 2006. ACM Press.
[24] C. Pollard . Higher-order categorial grammar. In M. Moortgat (ed.) Proceedings of the Conference on Categorial Grammars (CG2004), Montpellier, France, pp. 340–361, 2004.
[24] D. Clément . The natural dynamic semantics of Mini-Standard ML. In H. Ehrig , R. A. Kowalski , G. Levi and U. Montanari (eds), TAPSOFT, Vol.2, volume 250 Lecture Notes in Computer Science, pp. 67–81. Springer, 1987.
[24] D. Weise , R. Crew , M. Ernst and B. Steensgaard . Value dependence graphs: Representation without taxation. In POPL, pp. 297–310, 1994.
[24] O. Müller , T. Nipkow , D. von Oheimb and O. Slotosch . HOLCF = HOL + LCF. Journal of Functional Programming, 9:191–223, 1999.
[24] P. Hunter . Computational physiology and the physiome project, 2004. “http://nbcr.sdsc.edu/mcmregistration/pdf/Peter_Hunter.pdf”.
[24] T. M. Parks and D. Roberts . Distributed process networks in Java. In International Parallel and Distributed Processing Symposium, Nice, France, April 2003.
[24] T. Ott , J. Kemperman and M. Mathis , The stationary behavior of ideal TCP congestion avoidance. Research Report, 1996, available from T. Ott web page.
[24] V. van Oostrom . Finite family developments. In Proceedings of the 8th International Conference on Rewriting Techniques and Applications (RTA '97), volume 1232, in Lecture Notes in Computer Science, pp. 308–322, Sitges, June 1997.
[25] A. Ranta . Grammatical framework: a type-theoretical grammar formalism. Journal of Functional Programming, 14(2):145–189, 2004.
[25] D. Clément . A distributed architecture for programming environments. In R. N. Taylor (ed.), Proceedings of the Fourth ACM SIGSOFT Symposium on Software Development Environments, pp. 11–21, 1990.
[25] D. Scott . Outline of a mathematical theory of computation. In 4th Annual Princeton Conference on Information Sciences and Systems, pp. 169–176, 1970.
[25] M. E. Conway . Design of a separable transition-diagram compiler. Commun. ACM, 6(7):396–408, 1963.
[25] M. Weiser . Program slicing. In ICSE, pp. 439–449, 1981.
[25] S. Jbabdi , E. Mandonnet , H. Duffau , et al. Simulation of anisotropic growth of low-grade gliomas using diffusion tensor imaging. Magnetic Resonance Medicine, 54(3):616–624, 2005.
[25] T. Nipkow . Winskel is (almost) right: Towards a mechanized semantics. Formal Asp. Computing, 10(2):171–186, 1998.
[25] V. van Oostrom and R. de Vrijer . Four equivalent equivalences of reductions. In WRS'02, volume 70(6), ENTCS, December 2002.
[26] A. Ranta . Modular grammar engineering in GF. Research on Language and Computation, 5:133–158, 2007.
[26] B. Courcelle , G. Kahn and J. Vuillemin . Algorithmes d'equivalence et de reduction a des expressions minimales dans une classe d'equations recursives simples. In Proceedings of the 2nd Colloquium on Automata, Languages and Programming, pp. 200–213, London, UK. Springer-Verlag, 1974.
[26] D. Clément , J. Despeyroux , Th. Despeyroux , L. Hascoet and G. Kahn . Natural Semantics on the Computer. Technical Report RR416, I.N.R.I.A., june 1985.
[26] E. Konukoglu , O. Clatz , P.-Y. Bondiau , H. Delingette and N. Ayache . Extrapolating tumor invasion margins for physiologically determined radiotherapy regions. In Proc. of the 9th International Conference on Medical Image Computing and Computer Assisted Intervention (MICCAI'06), Part I, 2–4 October 2006, volume 4190, Lecture Notes in Computer Science, pp. 338–346, Springer-Verlag, 2006.
[26] G. Winskel . Event structure semantics for ccs and related languages. Technical report, DAIMI – AARhus University, April 1983.
[26] L. C. Paulson and T. Nipkow . Isabelle : a Generic Theorem Prover, volume 828, Lecture Notes in Computer Science. Springer-Verlag, 1994.
[26] P. Rizk , C. Kiddle and R. Simmonds . Improving gridFTP performance with split TCP connections. Proceeding of IEEE First International Conference on e-Science and Grid-Computing, 2005.
[26] V. Srini . An architectural comparison of dataflow systems. Computer, 19(3), 1986.
[26] W. Yang . A New Algorithm for Semantics-Based Program Integration. PhD thesis, Computer Science Department, University of Wisconsin, Madison, WI, Aug. 1990.
[27] A. Ranta . Grammatical Framework Homepage, 2008. digitalgrammars.com/gf.
[27] A. Sundararaj and D. Duchamp . Analytical characterization of the throughput of a split TCP connection. Technical Report, Stevens Institute of Technology, 2003.
[27] D. Clément , J. Despeyroux , Th. Despeyroux and G. Kahn . A simple applicative language: Mini-ML. In LISP and Functional Programming, pp. 13–27, 1986.
[27] D. Pichardie . Interprétation abstraite en logique intuitionniste : extraction d'analyseurs Java certifiés. PhD thesis, Université Rennes 1, 2005. (In French).
[27] E. W. Stark . An algebra of dataflow networks. Fundamenta Informaticae, 22(1–2):167–185, 1995.
[27] J. Darlington and M. Reeve . Alice a multi-processor reduction machine for the parallel evaluation cf applicative languages. In FPCA '81: Proceedings of the 1981 Conference on Functional Programming Languages and Computer Architecture, pp. 65–76, New York, NY, USA, 1981. ACM Press.
[27] M. I. Miller . Computational anatomy: shape, growth and atrophy comparison via diffeomorphisms. NeuroImage, 23(Supplement 1):S19–S33, 2004. Special Issue: Mathematics in Brain Imaging.
[27] W. Yang , S. Horwitz and T. Reps . Detecting program components with equivalent behaviors. TR-840, Computer Science Department, University of Wisconsin, Madison, WI, Apr. 1989.
[28] D. Clément , J. Heering , J. Incerpi , G. Kahn , P. Klint , B. Lang and V. Pascual . Preliminary design of an environment generator. Second annual review report: D9, GIPE, ESPRIT Project 348, January 1987.
[28] G. Plotkin . Structural operational semantics. Lecture notes DAIMI FN-19, Aarhus University, 1981. (reprinted 1991).
[28] J. Davies . POP-10 User's Manual. Technical Report CS R25, University of Western Ontario Computer Science Dept., 1976.
[28] M. Rayner , D. Carter , P. Bouillon , V. Digalakis and M. Wirén . The Spoken Language Translator. Cambridge University Press, Cambridge, 2000.
[28] R. Stephens . A survey of stream processing. Acta Informatica, 34(7), 1997.
[28] S. Nicolau , A. Garcia , X. Pennec , L. Soler and N. Ayache . An augmented reality system to guide radio-frequency tumor ablation. Computer Animation and Virtual World (previously the Journal of Visualization & Computer Animation), 16(1):1–10, 2005.
[28] W. Wei , C. Zhang , H. Zang , J. Kurose and D. Towsley . Inference and evaluation of Split-Connection Approaches in Cellular Data Networks. Proceedins of the ACM PAM, 2006.
[28] W. Yang , S. Horwitz and T. Reps . A program integration algorithm that accommodates semantics-preserving transformations. TOSEM, 1(3):310–354, July 1992.
[29] B. Stroustrup . The C++ Programming Language, Third Edition. Addison-Wesley, 1998.
[29] C. L. Talcott . Interaction semantics for components of distributed systems. In Formal Methods for Open Object-Based Distributed Systems (FMOODS), 1996.
[29] D. Clément , J. Incerpi and G. Kahn . CENTAUR: Towards a “software tool box” for programming environments. In F. Long (ed.), SEE, volume 467 Lecture Notes in Computer Science, pp. 287–304. Springer, 1989.
[29] D. Terrasse . Encoding natural semantics in Coq. In Proceedings of the Fourth International Conference on Algebraic Methodology and Software Technology, AMAST'95, Lecture Notes in Computer Science, pp. 230–244. Springer-Verlag, 1995.
[29] F. Xie , J. Hammond and D. L. Noneaker . Steady state analysis of a split-connection scheme for internet access through a wireless terminal. IEEE/ACM Transactions on Networking, 12(3), 2004.
[29] J. B. Dennis . Programming generality, parallelism, and computer architecture. In Information Processing 68, pp. 484–492. North Holland, 1969.
[29] X. Pennec , P. Fillard and N. Ayache . A Riemannian framework for tensor computing. International Journal of Computer Vision, 66(1):41–66, 2006. A preliminary version appeared as INRIA Research Report 5255, July 2004.
[2] A. Asperti , G. Bancerek and A. Trybulec (eds). Mathematical Knowledge Management, Third International Conference, MKM 2004, Bialowieza, Poland, September 19-21, 2004, Proceedings, volume 3119, Lecture Notes in Computer Science. Springer, 2004.
[2] A. Benveniste , P. Caspi , P. L. Guernic and N. Halbwachs . Dataflow synchronous languages. In J. W. d. Bakker , W.-P. d. Roever and G. Rozenberg , (eds), A Decade of Concurrency – Reflections and Perspectives, Volume 803 Lecture Notes in Computer Science, pp. 1–45. Springer-Verlag, 1994.
[2] A. Carle and M. Fagan . ADIFOR 3.0 overview. Technical Report CAAMTR-00-02, Rice University, 2000.
[2] A. Cohen , M. Duranton , C. Eisenbeis , C. Pagetti , F. Plateau and M. Pouzet . N-sychronous Kahn networks. In 33th ACM Symp. on Principles of Programming Languages (PoPL'06), pp. 180–193, Charleston, South Carolina, January 2006.
[2] A. Rowstron and P. Druschel . Pastry: scalable, distributed object location and routing for large scale peer-to-peer systems. IFIP/ACM International Conference on Distributed System Platforms (Middleware), Heidelberg, Germany pp. 329–350, November 2001.
[2] B. Alpern , M. Wegman , and F. Zadeck . Detecting equality of variables in programs. In POPL, pp. 1–11, 1988.
[2] B. Beckert , R. Hähnle and P. Schmitt . Verification of Object-Oriented Software: The KeY Approach, volume 4334 Lecture Notes in Computer Science. Springer-Verlag, 2006.
[2] D. Caucal , On infinite terms having a decidable monadic theory. MFCS 2002, Lecture Notes in Computer Science 2420, pp. 165–176, Springer-Verlag, 2002.
[2] D. Clément , J. Despeyroux , T. Despeyroux and G. Kahn . A simple applicative language: Mini-ML. In Proc. ACM Conf. Lisp and Functional Programming, pp. 13–27, 1986.
[2] E. Altman , K. Avrachenkov and C. Barakat . A stochastic model of TCP/IP with stationary random losses. IEEE/ACM Transactions on Networking, 13; 356–369, 2005.
[2] G. Barthe , G. Dufay , L. Jakubiec , S. Melo de Sousa and B. Serpette . A formal executable semantics of the JavaCard platform. In D. Sands (ed.) Proceedings of ESOP'01, volume 2028 Lecture Notes in Computer Science, pp. 302–319. Springer-Verlag, 2001.
[2] G. Berry , Stable models of typed lambda-calculi. In Proc. ICALP 1978, Lecture Notes in Computer Science 62 Springer-Verlag (1978).
[2] H. Barendregt . Handbook of Mathematical Logic, chapter the type free lambda calculus. In North-Holland, 1977.
[2] I. Attali , D. Caromel and A. L. Wendelborn . From a formal dynamic semantics of Sisal to a Sisal environment. In HICSS (2), pp. 266–267, 1995.
[2] J.-P. Banâtre , P. Fradet and D. Le Métayer . Gamma and the chemical reaction model: Fifteen years after. In Multiset Processing, volume 2235 of Lecture Notes in Computer Science, pp. 17–44. Springer-Verlag, 2001.
[2] L. Axel , A. Montillo and D. Kim . Tagged magnetic resonance imaging of the heart: a survey. Medical Image Analysis, 9(4):376–393, 2005.
[2] P. Audebaud and C. Paulin-Mohring . Proofs of randomized algorithms in Coq. To appear in Science of Computer Programming. Extended version of [1].
[2] S. Abramsky . A generalized Kahn principle for abstract asynchronous networks. In Mathematical Foundations of Programming Semantics, 5th International Conference, pp. 1–21. Springer-Verlag, 1989.
[2] T. H. Clutton-Brock . The Evolution of Parental Care, University Press, Oxford, 1991.
[2] W.P. De Roever , Operational and mathematical semantics for first-order recursive program schemas, (private communication).
[2] Y. Lazebnik . Can a biologist fix a radio? Or, what I learned while studying apoptosis. Cancer Cell 2:179–182, 2002.
[30] D. Clément , V. Prunet and F. Montagnac . Integrated software components: A paradigm for control integration. In A. Endres and H. Weber (eds), Software Development Environments and CASE Technology, volume 509, Lecture Notes in Computer Science, pp. 167–177. Springer, 1991.
[30] J. B. Dennis . First version of a data flow procedure language. In Programming Symposium, Proceedings Colloque sur la Programmation, volume 19 of Lecture Notes in Computer Science, pp. 362–376, Springer-Verlag, 1974.
[30] J. van den Berg and B. Jacobs . The loop compiler for Java and JML. In TACAS 2001, pp. 299–312. Springer-Verlag, 2001.
[30] The Coq Development Team . The Coq Proof Assistant Reference Manual. pauillac.inria.fr/coq/, 1999.
[30] W. Thies , M. Karczmarek and S. Amarasinghe . StreamIt: A language for streaming applications. In 11th International Conference on Compiler Construction, volume 2304, Lecture Notes in Computer Science, Grenoble, France, 2002, Springer-Verlag.
[30] X. Pennec and S. Joshi (eds). Proceedings of the First International Workshop on Mathematical Foundations of Computational Anatomy–Geometrical and Statistical Methods for Modelling Biological Shape Variability, Copenhagen, Denmark, October 2006.
[31] A. Trybulec . The Mizar Homepage. http://mizar.org/, 2006.
[31] D. von Oheimb . Analyzing Java in Isabelle/HOL, Formalization, Type Safety, and Hoare Logic. PhD thesis, Technische Universität München, 2000.
[31] J. B. Dennis , J. B. Fosseen and J. P. Linderman . Data flow schemas. In G. Goos and J. Hartmanis (eds), International Symposium on Theoretical Programming, volume 5, Lecture Notes in Computer Science, pp. 187–216, Springer-Verlag, 1974.
[31] J.-M. Peyrat , M. Sermesant , H. Delingette , et al. Towards a statistical atlas of cardiac fiber structure. In Proc. of the 9th International Conference on Medical Image Computing and Computer Assisted Intervention (MICCAI'06), Part I, 2–4 October 2006, volume 4190, Lecture Notes in Computer Science, pp. 297–304. Springer-Verlag, 2006.
[31] W. Thies , M. Karczmarek , J. Sermulins , R. Rabbah and S. Amarasinghe . Teleport messaging for distributed stream programs. In PPoPP, Chicago, Illinois, USA, 2005. ACM.
[31] Y. Coscoy , G. Kahn and L. Théry . Extracting text from proofs. In M. Dezani-Ciancaglini and G. D. Plotkin (eds), TLCA, volume 902, Lecture Notes in Computer Science, pp. 109–123. Springer, 1995.
[32] A. Turjan , B. Kienhuis and E. Deprettere . Solving out-of-order communication in Kahn process networks. Journal on VLSI Signal Processing-Systems for Signal, Image, and Video Technology, 2003.
[32] G. Picinbono , H. Delingette and N. Ayache . Non-linear anisotropic elasticity for real-time surgery simulation. Graphical Models, 65(5):305–321, 2003.
[32] G. Winskel . The Formal Semantics of Programming Languages, an introduction. Foundations of Computing. The MIT Press, 1993.
[32] J. B. Dennis . A language design for structured concurrency. In J. H. Williams and D. A. Fisher (eds), Proceedings of the DoD Sponsored Workshop on Design and Implementation of Programming Languages, volume 54, Lecture Notes in Computer Science, pp. 231–242. Springer-Verlag, 1977.
[32] J. Coutaz . The Box, a Layout Abstraction for User Interface Toolkits. Technical Report CMU-CS-84-167, Carnegie Mellon University, 1984.
[32] M. Wenzel . Isar – a generic interpretative approach to readable formal proof documents. In Y. Bertot , G. Dowek , A. Hirschowitz , C. Paulin and L. Théry (eds) Theorem Proving in Higher Order Logics, TPHOLs'99, volume 1690 Lecture Notes in Computer Science, 1999.
[33] A. Quarteroni and L. Formaggia . Mathematical modeling and numerical simulation of the cardiovascular system. In N. Ayache (ed.) Computational Models for the Human Body, pp. 3–128. Elsevier, 2004.
[33] F. Wiedijk . Formal proof sketches. In Types for Proofs and Programs, volume 3085 Lecture Notes in Computer Science, pp. 378–393. Springer, 2004.
[33] J. B. Dennis . Stream Data Types for Signal Processing. Computation Structures Group Memo 36, MIT LCS, October 1994.
[33] Th. Despeyroux . Executable specification of static semantics. In G. Kahn , D. B. MacQueen and G. D. Plotkin , editors, Semantics of Data Types, volume 173, Lecture Notes in Computer Science, pp. 215–233. Springer, 1984.
[34] A. van Deursen , J. Heering and P. Klint (eds). Language Prototyping: An Algebraic Specification Approach, volume 5, AMAST Series in Computing. World Scientific, 1996.
[34] D. Rey , G. Subsol , H. Delingette and N. Ayache . Automatic detection and segmentation of evolving processes in 3D medical images: Application to multiple sclerosis. Medical Image Analysis, 6(2):163–179, 2002.
[34] J. B. Dennis and D. P. Misunas . A preliminary architecture for a basic data-flow processor. In ISCA '75: Proceedings of the 2nd Annual Symposium on Computer Architecture, pp. 126–132, New York, NY, USA, 1975. ACM Press.
[35] A. van Deursen , P. Klint and F. Tip . Origin tracking. Journal of Symbolic Computing 15(5–6):523–545, 1993.
[35] D. P. Friedman and D. S. Wise . Cons should not evaluate its arguments. In S. Michaelson and R. Milner (eds), Automata, Languages and Programming, pp. 257–284. Edinburgh University Press, 1976.
[35] D. Rivière , J.-F. Mangin , D. Papadopoulos-Orfanos , et al. Automatic recognition of cortical sulci of the human brain using a congregation of neural networks. Medical Image Analysis, 6(2):77–92, 2002.
[36] M. J. C. Gordon , A. J. R. G. Milner , L. Morris , M. C. Newey and C. P. Wadsworth . A metalanguage for interactive proof in LCF. In Fifth ACM Symposium on Principles of Programming Languages, New York, 1978. ACM Press.
[36] M. Sermesant , H. Delingette and N. Ayache . An electromechanical model of the heart for image analysis and simulation. IEEE Transactions in Medical Imaging, 25(5):612–625, 2006.
[36] V. Donzeau-Gouge , G. Huet , G. Kahn , B. Lang and J.J. Lévy . A structure oriented program editor: a first step towards computer assisted programming. In International Computing Symposium. North Holland, 1975.
[37] J. R. Gurd , C. C. Kirkham and I. Watson . The Manchester prototype dataflow computer. Commun. ACM, 28(1):34–52, 1985.
[37] M. Sermesant , P. Moireau , O. Camara , et al. Cardiac function estimation from MRI using a heart model and data assimilation: Advances and difficulties. Medical Image Analysis, 10(4):642–656, 2006.
[37] V. Donzeau-Gouge , G. Kahn and B. Lang . On the formal definition of ADA. In N. D. Jones (ed.), Semantics-Directed Compiler Generation, volume 94 Lecture Notes in Computer Science, pp. 475–489. Springer, 1980.
[38] N. Halbwachs , P. Caspi , P. Raymond and D. Pilaud . The synchronous dataflow programming language LUSTRE. Proceedings of the IEEE, 79(9):1305–1320, Sept. 1991.
[38] R. Sierra , M. Bajka and G. Székely . Pathology design for surgical training simulators. In International Symposium on Surgery Simulation and Soft Tissue Modeling, volume 2673, Lecture Notes in Computer Science, pp. 375–384. Springer-Verlag, 2003.
[38] V. Donzeau-Gouge , G. Kahn , B. Lang and B. Mélèse . Documents structure and modularity in mentor. In Software Development Environments (SDE), pp. 141–148, 1984.
[39] E. Harold . Java I/O, 2nd Edition. O'Reilly Media, 2006.
[39] K. R. Swanson , E. C. Alvord and J. D. Murray . Virtual brain tumours (gliomas) enhance the reality of medical imaging and highlight inadequacies of current therapy. British Journal of Cancer, 86(1):14–18, 2002.
[39] V. Donzeau-Gouge , G. Kahn , B. Lang , B. Mélèse and E. Morcos . Outline of a tool for document manipulation. In IFIP Congress, pp. 615–620, 1983.
[3] A. Colmerauer , Prolog and infinite trees, logic programming, In: W. Clark and S. Tarnlund (eds.), pp. 153–172. Academic Press, 1982.
[3] C. Ferris and J. Farrell . What are web services? CACM 46(6):31, 2003.
[3] D. A. Adams . A Computation Model with Data Flow Sequencing. PhD thesis, Computer Science Dept, Stanford University, December 1968. Technical Report CS-117.
[3] E. Klipp , R. Herwig , A. Kowald , C. Wierling and H. Lehrach . Systems Biology in Practice. Wiley, 2005.
[3] E. M. Bender and D. Flickinger . Rapid prototyping of scalable grammars: Towards modularity in extensions to a language-independent core. In Proceedings of the 2nd International Joint Conference on Natural Language Processing IJCNLP-05 (Posters/Demos), Jeju Island, Korea, 2005.
[3] G. Barthe , M. Ruys and H. Barendregt . A two-level approach towards lean proof-checking. In TYPES '95: Selected papers from the International Workshop on Types for Proofs and Programs, London, UK, pp. 16–35. Springer-Verlag, 1996.
[3] G. Berry . Bottom-up computation of recursive programs. Revue Française d'Automatique, Informatique et Recherche Opérationnelle, 10(3):47–82, 1976.
[3] G. Berry and P.-L. Curien , Sequential algorithms on concrete data structures, Theoretical Computer Science 20:265–321 (1982).
[3] G. Corliss , C. Faure , A. Griewank , L. Hascoët and U. Naumann (eds). Automatic Differentiation of Algorithms, from Simulation to Optimization. LNCSE. Springer, 2002. Selected papers from AD2000, Nice, June 2000.
[3] H. Barendregt . The Lambda Calculus, Its Syntax and Semantics. North-Holland, 1984.
[3] I. Attali , J. Chazarain and S. Gilette . Incremental evaluation of natural semantics specification. In M. Bruynooghe and M. Wirsing (eds), PLILP, volume 631, Lecture Notes in Computer Science, pp. 87–99. Springer, 1992.
[3] J. Engelfriet , A note on infinite trees, Information Processing Letters 1:229–232, 1972.
[3] J.-P. Banâtre , P. Fradet and Y. Radenac . Principles of chemical programming. In S. Abdennadher and C. Ringeissen (eds), Proceedings of the 5th International Workshop on Rule-Based Programming (RULE 2004), volume 124 of ENTCS, pp. 133–147. Elsevier, June 2005.
[3] K. B. Athreya and P. Ney . A new approach to the limit theory of recurrent Markov chains. Transactions of the American Mathematical Society, 1978.
[3] L. Damas . Type Assignment in Programming Languages. PhD thesis, University of Edinburgh, 1984.
[3] M. Doebeli and C. Hauert . Models of cooperation based on Prisoner's dilemma and Snowdrift games. In Ecology Letters, 8:748–756, 2005.
[3] N. Ayache . Epidaure: a research project in medical image analysis, simulation and robotics at INRIA. IEEE Trans. on Medical Imaging, 22(10):1185–1201, 2003.
[3] P. Borras , D. Clément , T. Despeyroux , et al. Centaur: the system. In Software Engineering Notes, volume 13(5). Third Symposium on Software Development Environments, 1988.
[3] R. Bornat and B. Sufrin . Animating formal proof at the surface: The Jape proof calculator. Computer Journal, 42(3):177–192, 1999.
[3] T. Amtoft . Slicing for modern program structures: a theory for eliminating irrelevant loops. Information Processing Letters, 106:45–51, 2008.
[3] Y. Bertot . Filters on coinductive streams, an application to Eratos thenes'sieve. In P. Urzyczyn (ed.) International Conference of Typed Lambda Calculi and Applications, volume 3461, Lecture Notes in Computer Science, pp. 102–115. Springer-Verlag, 2005.
[40] D. W. Thompson . On Growth and Form. Cambridge University Press, 1917.
[40] P. Henderson and J. H. Morris . A lazy evaluator. In Third ACM Symposium on Principles of Programming Languages, pp. 123–42, New York, 1976. ACM Press.
[40] V. Donzeau-Gouge , B. Lang and B. Mélèse . Practical applications of a syntax directed program manipulation environment. In ICSE, pp. 346–357, 1984.
[41] C. Hewitt , P. Bishop , R. Steiger , I. Greif , B. Smith , T. Matson and R. Hale . Behavioral semantics of nonrecursive control structures. In Programming Symposium, Proceedings Colloque sur la Programmation, volume 19, Lecture Notes in Computer Science, pp. 385–407. Springer-Verlag, 1974.
[41] J. Heering , P. R. H. Hendriks , P. Klint and J. Rekers . The syntax definition formalism SDF – reference manual. SIGPLAN Notices, 24(11):43–75, 1989.
[41] P. M. Thompson , M. I. Miller , J. T. Ratnanather , R. A. Poldrack and T. E. Nichols . Guest editorial. NeuroImage, 23(Supplement 1):S1–S1, 2004. Special Issue: Mathematics in Brain Imaging.
[42] G. Kahn and G. D. Plotkin . Domaines concrets. INRIA Rapport 336, INRIA, 1978.
[42] J. Heering , G. Kahn , P. Klint and B. Lang . Generation of interactive programming environments. In ESPRIT '85, Status Report of Continuing Work, Part I, pp. 467–477. North-Holland, 1986.
[42] P. M. Thompson , K. M. Hayashi , E. R. Sowell , et al. Mapping cortical change in Alzheimer's disease, brain development, and schizophrenia. NeuroImage, 23(Supplement 1):S2–S18, 2004. Special Issue: Mathematics in Brain Imaging.
[43] G. Kahn and G. D. Plotkin . Concrete domains. Theoret. Comput. Sci., 121(1–2):187–277, 1993.
[43] J. Heering and P. Klint . Towards monolingual programming environments. ACM Transactions on Programming Languages and Systems, 7(2):183–213, April 1985.
[43] K. V. Leemput , F. Maes , D. Vandermeulen and P. Suetens . A unifying framework for partial volume segmentation of brain MR images. IEEE Transactions in Medical Imaging, 22(1):105–19, 2003.
[44] G. Kahn . An approach to systems correctness. In SOSP '71: Proceedings of the Third ACM Symposium on Operating Systems Principles, pp. 86–94, New York, NY, USA, 1971. ACM Press.
[44] J. Heering and P. Klint . Prehistory of the ASF+SDF system (1980–1984). In M. G. J. van den Brand , A. van Deursen , T. B. Dinesh , J. Kamperman and E. Visser (eds), Proceedings of ASF+SDF95 A workshop on Generating Tools from Algebraic Specifications, number P9504 in Technical Report. Programming Research Group, University of Amsterdam, 1995.
[44] T. Vercauteren , A. Perchant , G. Malandain , X. Pennec and N. Ayache . Robust mosaicing with correction of motion distortions and tissue deformation for in vivo fibered microscopy. Medical Image Analysis, 10(5):673–692, 2006. Annual Medical Image Analysis (MedIA) Best Paper Award 2006.
[45] G. Kahn . A Preliminary Theory for Parallel Programs. Technical Report Rapport Laboria no. 6, IRIA Rocquencourt, January 1973.
[45] J. Heering , P. Klint and J. Rekers . Incremental generation of parsers. IEEE Transactions on Software Engineering, 16(12):1344–1350, 1990.
[46] G. Kahn . The semantics of a simple language for parallel programming. In Information Processing 74, Proceedings of the IFIP Congress 74, pp. 471–475. Elsevier North Holland, 1974.
[46] I. Jacobs , F. Montignac , J. Bertot , D. Clément and V. Prunet . The Sophtalk Reference Manual. Technical Report 149, INRIA, February 1993.
[47] G. Kahn . An approach to system correctness. In SOSP, pp. 86–94, 1971.
[47] G. Kahn and D. B. MacQueen . Coroutines and networks of parallel processes. In B. Gilchrist (ed.), Information Processing 77, pp. 993–998. North Holland, 1977.
[48] G. Kahn (ed.) Semantics of Concurrent Computation, Proceedings of the International Sympoisum, Evian, France, July 2–4, 1979, volume 70, Lecture Notes in Computer Science. Springer, 1979.
[48] G. Kahn and G. Plotkin . Concrete Data-types. first draft manuscript, December 1975.
[49] G. Kahn . Natural semantics. In F.-J. Brandenburg , G. Vidal-Naquet and M. Wirsing (eds), STACS, volume 247, Lecture Notes in Computer Science, pp. 22–39. Springer, 1987.
[49] R. M. Karp and R. E. Miller . Properties of a model for parallel computations: Determinacy, termination, queueing. SIAM J. Appl. Maths, 14(6):1390–1411, 1966.
[4] A. Appel and D. B. MacQueen . Standard ml of new jersey. In J. Maluszynski and M. Wirsing (eds) Programming Language Implementation and Logic Programming, Proceedings of the 3rd International Symposium, volume 528 Lecture Notes in Computer Science, pp. 1–13. Springer Verlag, 1991.
[4] Aho, Sethi, Ullman . Compiler Writing: Principles Programming and Tools, Addison Wesley, 1986.
[4] B. Courcelle , Fundamental properties of infinite trees, Theoretical Computer Science, 25:95–169, 1983.
[4] Bescherelle . La conjugaison pour tous. Hatier, 1997.
[4] C. Faure and U. Naumann . Minimizing the tape size. In [3], chapter VIII, pp. 293–298. 2002.
[4] C.-O. Ewald , J. M. McNamara and A. Houston . Parental care as a differential game: a dynamic extension of the Houston–Davis game. Applied Mathematics and Computations, 190:1450–1465, 2007.
[4] F. Baccelli and P. Bremaud . Elements of Queueing Theory, 2nd ed. Wiley, 2003.
[4] G. Berry and J.-J. Lévy . Minimal and optimal computations of recursive programs. JACM, 26(1):148–175, January 1979.
[4] G. Berry and P.-L. Curien , Theory and practice of sequential algorithms: the kernel of the applicative language CDS. In Algebraic Methods in Semantics, M. Nivat , J. Reynolds (eds), Cambridge University Press, pp. 35–87 (1985).
[4] G. Kahn , A preliminary theory for parallel programs. (Rapport Laboria no. 6, January 1973).
[4] I. Attali , C. Courbis , P. Degenne , A. Fau , J. Fillon , Chr. Held , D. Parigot and C. Pasquie . Aspect and XML-oriented semantic framework generator: Smarttools. In Second Workshop on Language Descriptions, Tools and Applications, LDTA'02, volume 65 Electronic Notes in Theoretical Computer Science (ENTCS), pp. 1–20. Springer, 2002.
[4] J. D. Brock and W. B. Ackerman . Scenarios, a model of non-determinate computation. In Conference on Formal Definition of Programming Concepts, volume 107, Lecture Notes in Computer Science, pp. 252–259. Springer-Verlag, 1981.
[4] J.-P. Banâtre , P. Fradet and Y. Radenac . Generalised multisets for chemical programming. Mathematical Structures in Computer Science, 16(4):557–580, 2006.
[4] L. Damas and R. Milner . Principal type schemes for functional programs. In Proc. 9th ACM Symp. Principles of Programming Languages, pp. 207–212, 1982.
[4] M. Lesk . Online Data and Scientific Progress: Content in Cyberin-frastructure. http://archiv.twoday.net/stories/337419/, 2004 [Accessed 6 December 2005].
[4] N. Ayache (ed.) Computational Models for the Human Body. Handbook of Numerical Analysis (Ph. Ciarlet series editor). Elsevier, 2004. 670 pages.
[4] P. Borras , D. Clement , Th. Despeyrouz , J. Incerpi , G. Kahn , B. Lang , and V. Pascual . CENTAUR: The system. In Proceedings of the ACM SIGSOFT/SIGPLAN Software Engineering Symposium on Practical Software Development Environments (PSDE), volume 24, pp. 14–24, New York, NY, 1989. ACM Press.
[4] R. Cartwright and M. Felleisen . The semantics of program dependence. In PLDI, pp. 13–27, 1989.
[4] R. Feynman , R. Leighton and E. Hutchings . He fixes radios by thinking. In Surely You're Joking, Mr. Feynman!: Adventures of a Curious Character. W.W. Norton, 1985.
[4] S. Berghofer and T. Nipkow . Executing higher order logic. In P. Callaghan , Z. Luo , J. McKinna and R. Pollack (eds) TYPES, volume 2277, Lecture Notes in Computer Science, pp. 24–40. Springer-Verlag, 2000.
[4] Y. Bertot and P. Castéran . Interactive Theorem Proving and Program Development. Springer-Verlag, 2004.
[50] G. Kahn , B. Lang , B. Mélèse and E. Morcos . Metal: A formalism to specify formalisms. Science of Computer Programming, 3(2):151–188, 1983.
[50] J. Kelly , C. Lochbaum and V. Vyssotsky . A block diagram compiler. Bell System Tech. J., 40(3):669–676, May 1961.
[51] G. Kahn and D. B. MacQueen . Coroutines and networks of parallel processes. In IFIP Congress, pp. 993–998, 1977.
[51] S. Kleene . Introduction to Metamathematics. Van Nostrand, 1952.
[52] G. Kopec . A high-level block-diagram signal processing language. In IEEE International Conference on Acoustics, Speech, and Signal Processing, pp. 684–687, 1979.
[52] P. Klint . An overview of the summer programming language. In Conference Record of the 7th ACM Symposium on Principles of Programming Languages (POPL'80), pp. 47–55, 1980.
[53] P. J. Landin . A correspondence between ALGOL 60 and Church's lambda-notation: Part I. Commun. ACM, 8(2):89–101, 1965.
[53] P. Klint . Formal language definitions can be made practical. In Algorithmic Languages, pp. 115–132, 1981.
[54] D. C. Luckham , D. M. R. Park and M. S. Paterson . On formalized computer programs. J. System Sci., 4(3):220–249, 1970.
[54] P. Klint . A Survey of Three Language-independent Programming Environments. RR 257, INRIA, 1983.
[55] D. B. MacQueen , P. Wadler and W. Taha . How to add laziness to a strict language without even being odd. In Proceedings of the 1998 ACM Workshop on ML, pp. 24–30, September 1998. Baltimore, MD.
[55] P. Klint . A Study in String Processing Languages, volume 205 of Lecture Notes in Computer Science. Springer-Verlag, 1985. Based on the dissertation From Spring to Summer, defended at the Technical University Eindhoven, 1982.
[56] J. McCarthy , P. W. Abrahams , D. J. Edwards , T. P. Hart and M. E. Levin . LISP 1.5 Programmer's Manual. MIT Press, 1962.
[56] P. Klint . A meta-environment for generating programming environments. ACM Transactions on Software Engineering and Methodology, 2(2):176–201, April 1993.
[57] J. McCarthy . Towards a mathematical science of computation. In Proceedings of the IFIP Congress 1962, pp. 21–28. North-Holland, 1962.
[57] J. W. C. Koorn and H. C. N. Bakker . Building an Editor from Existing Components: an Exercise in Software Re-use. Technical Report P9312, Programming Research Group, University of Amsterdam, 1993.
[58] H. Korte , H. Joosten , V. Tijsse , A. Wammes , J. Wester , Th. Kuhne and Chr. Thies . Design of a LOTOS Simulator: Centaur from a user's Perspective. Fifth annual review report: D5, GIPE II, ESPRIT project 2177, 1993.
[58] J. McCarthy . A basis of a mathematical theory of computation. In P. Braffort and D. Hirshberg (eds), Computer Programming and Formal Systems, pp. 33–70. North-Holland, 1963.
[59] B. Lang . Deterministic techniques for efficient non-deterministic parsers. In J. Loeckx (ed.) ICALP, volume 14, Lecture Notes in Computer Science, pp. 255–269. Springer, 1974.
[59] M. D. McIlroy . Coroutines. unpublished note, May 1968.
[5] A. E. Ashcroft . Program proving without tears. In G. Huet and G. Kahn (eds) Symposium on Proving and Improving Programs, pp. 99–111. INRIA Rocquencourt, July 1975.
[5] B. Bringert . Embedded Grammars. MSc Thesis, Department of Computing Science, Chalmers University of Technology, 2004.
[5] B. Courcelle , Equivalences and transformations of regular systems. Applications to recursive program schemes and grammars. Theoretical Computer Science, 42:1–122, 1986.
[5] Bandai . Tamagotchi Connection. http://www.tamagotchi.com
[5] C. Dubois and V. Ménissier-Morain . Certification of a type inference tool for ML: Damas-Milner within Coq. Journal of Automated Reasoning, 23:319–346, 1999.
[5] C. Faure and Y. Papegay . Odyssée User's Guide. Version 1.7. Technical report 224, INRIA, 1998.
[5] Coq homepage . pauillac.inria.fr/coq/, 1999.
[5] F. Baccelli , A. Chaintreau , Z. Liu , A. Riabov and S. Sahu . Scalability of reliable group communication using overlays. Proceedings of the IEEE Infocom, February 2004.
[5] G. Boudol . Computational semantics of term rewriting systems. In Algebraic methods in Semantics. Cambridge University Press, 1985.
[5] I. Attali , C. Courbis , P. Degenne , A. Fau , D. Parigot and C. Pasquier . Smarttools: a generator of interactive environment tools. Electr. Notes Theoritical Computer Science, 44(2), 2001.
[5] J. Gray , D. T. Liu , M. Nieto-Santisteban , A. S. Szalay , D. De Wiit and G. Heber . Scientific Data Management in the Coming Decade. Technical Report MSR-TR-2005-10, Microsoft Research, 2005.
[5] J. Kral , Equivalence of modes and the equivalence of finite automata, Algol Bulletin 35:34–35, 1973.
[5] J.-P. Banâtre , P. Fradet and Y. Radenac . Programming self-organizing systems with the higher-order chemical language. International Journal of Unconventional Computing, 2007.
[5] M. Broy . Functional specification of time-sensitive communicating systems. ACM Transactions on Software Engineering and Methodology, 2(1):1–46, 1993.
[5] N. Ayache , J.-P. Boissel , S. Brunak , et al. Towards virtual physiological human: Multilevel modelling and simulation of the human anatomy and physiology. Virtual Physiological Human: White paper, EC – DG INFSO and DG JRC, 2006.
[5] R. A. Fisher . The Genetical Theory of Natural Selection, University Press, Oxford, 1930.
[5] R. Cartwright and M. Felleisen , Observable sequentiality and full abstraction. In Proc. POPL 1992 (1992).
[5] R. Cytron , J. Ferrante , B. Rosen , M. Wegman and F. Zadeck . An efficient method of computing static single assignment form. In POPL, pp. 25–35, 1989.
[5] S. Boulmé and G. Hamon . Certifying synchrony for free. In International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), volume 2250, Lecture Notes in Artificial Intelligence, La Havana, Cuba, December 2001. Springer-Verlag, 2001. Short version of A clocked denotational semantics for Lucid-Synchrone in Coq, available as a Technical Report (LIP6), at www.lri.fr/∼pouzet.
[5] Y. Bertot . A Certified Compiler for an Imperative Language. Research Report RR-3488, INRIA, 1998.
[5] Y. Coscoy , G. Kahn and L. Théry . Extracting text from proofs. In Typed Lambda Calculi and Applications TLCA'95, Edinburgh.
[60] B. Lang . On the usefulness of syntax directed editors. In R. Conradi , T. Didriksen and D. H. Wanvik (eds) Advanced Programming Environments, volume 244, Lecture Notes in Computer Science, pp. 47–51. Springer, 1986.
[60] M. D. McIlroy . Squinting at power series. Software Pract. Exper., 20:661–683, 1990.
[61] B. Lang . The virtual tree processor. In J. Heering J. Sidi and A. Verhoog (eds) Generation of Interactive Programming Environments, Intermediate Report, number CS-R8620 in Technical Report. Centrum voor Wiskunde en Informatica, 1986.
[61] M. D. McIlroy . Power Series as Lazy Streams. Technical Report BL011276-970313-02TMS, Bell Laboratories, Lucent Technologies, 1997.
[62] J. L. Lions . ARIANE 5: Flight 501 Failure, Report by the Inquiry Board. http://homepp..inf.ed.ac.uk/perdita/Book/ariane5rep.html, 1996. Last visit January 2007.
[62] M. D. McIlroy . Power series, power serious. J. Funct. Program., 9(3):325–337, May 1999.
[63] Meta-Environment web pp. , Last visit March 2008. http://www.meta-environment.org.
[63] R. Milner . Implementation and applications of Scott's logic for computable functions. In Proceedings of ACM Conference on Proving Assertions About Programs, pp. 1–6, New York, NY, USA, 1972. ACM.
[64] E. van der Meulen . Deriving incremental implementations from algebraic specifications. In M. Nivat , Ch. Rattray , T. Rus and G. Scollo (eds) AMAST, Workshops in Computing, pp. 277–286. Springer, 1991.
[64] R. Milner . Processes: A mathematical model of computing agents. In Proceedings of the Colloquium in Mathematical Logic, pp. 157–173. North-Holland, 1973.
[65] E. Morcos-Chounet and A. Conchon . PPML: a general purpose formalism to specify prettyprinting. In H.-J. Kugler (ed.) Information Processing 86 pp. 583–590. Elsevier, 1986.
[65] R. Milner and R. Weyrauch . Proving compiler correctness in a mechanized logic. In Machine Intelligence 7. Edinburgh University Press, 1972.
[66] P. A. Olivier . Debugging distributed applications using a coordination architecture. In D. Garlan and D. Le Métayer (eds) COORDINATION, volume 1282, Lecture Notes in Computer Science, pp. 98–114. Springer, 1997.
[66] S. Peyton-Jones (ed.) Haskell98, Languages and Libraries, The Revised Report. Cambridge University Press, 2003.
[67] D. C. Oppen . Prettyprinting. ACM Transactions on Programming Languages and Systems, 2(4):465–483, 1980.
[67] E. D. Reilly . Milestones in Computer Science and Information Technology. Greenwood Press, 2003.
[68] J. Reppy and E. Gansner . The Standard ML Basis Library. Cambridge University Press, 2006.
[68] Sophtalk web pp. , Last visit December 2006. http://www-sop.inria.fr/croap/sophtalk/sophtalk.html.
[69] D. M. Ritchie . A stream input-output system. AT&T Bell Laboratories Tech. J., 63(8):1897–1910, 1984.
[69] L. Théry , Y. Bertot and G. Kahn . Real theorem provers deserve real userinterfaces. In SDE 5: Proceedings of the Fifth ACM SIGSOFT Symposium on Software Development Environments, pp. 120–129, New York, NY, USA, 1992. ACM Press.
[6] A. Church . The Calculi of Lambda-Conversion. Princeton University Press – Oxford University Press, 1941.
[6] A. E. Ashcroft and W. W. Wadge . Lucid – a formal system for writing and proving programs. SIAM J. Comput., 5:519–526, 1976.
[6] A. P. Cootes , S. H. Muggleton and M. J. Sternberg . The automatic discovery of structural principles describing protein fold space. J. Mol. Biol. 330(4):839–850, 2003.
[6] B. Courcelle , Recursive applicative program schemes. In: J. Van Leeuwen (ed.), Handbook of Theoretical Computer Science, Volume B, pp. 459–492. Elsevier, 1990.
[6] C. A. Gunter . Semantics of Programming Languages. MIT Press, 1992.
[6] C.H Lewis and B. K. Rosen , Recursively defined data types: part 1. Proceedings of the 1st annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 125–138. ACM, New York, 1973.
[6] D. A. Burke and K. Johannisson . Translating Formal Software Specifications to Natural Language / A Grammar-Based Approach. In P. Blache , E. Stabler , J. Busquets and R. Moot (eds) Logical Aspects of Computational Linguistics (LACL 2005), volume 3402 LNCS/LNAI, pp. 51–66. Springer-Verlag, 2005.
[6] F. Baccelli , G. Carofiglio and S. Foss . Proxy Caching in split TCP: Dynamics, Stability and Tail Asymptotics, INRIA Report, July 2007.
[6] F. Hamelin . Jeux dynamiques en écologie du comportement. thèse de doctorat, Université de Nice, soutenue le 4 juillet 2007.
[6] H. B. Curry . Some logical aspects of grammatical structure. In R. O. Jakobson (ed.) Structure of Language in its Mathematical Aspects. Proceedings of the 12th Symposium in Applied Mathematics, pp. 56–68, 1961.
[6] J. A. Bergstra , J. Heering and P. Klint (eds), Algebraic Specification. ACM Press/Addison-Wesley, 1989.
[6] J. Ferrante , K. Ottenstein and J. Warren . The program dependence graph and its use in optimization. TOPLAS, 3(9):319–349, 1987.
[6] J.-P. Banâtre and D. Le Métayer . Programming by multiset transformation. Communications of the ACM (CACM), 36(1):98–111, 1993.
[6] M. Broy and G. Stefanescu . The algebra of stream processing functions. Theoretical Computer Science, 258:99–129, 2001.
[6] M. E. Belik , T. P. Usyk and A. D. McCulloch . Computational methods for cardiac electrophysiology. In N. Ayache (ed.) Computational Models for the Human Body, pp. 129–187. Elsevier, 2004.
[6] P. Tonella and A. Potrich . Reverse Engineering of Object-Oriented Code. Springer, 2005.
[6] R. Cartwright , P.-L. Curien and M. Felleisen , Fully abstract semantics for observably sequential languages, Information and Computation 111(2):297–401 (1994).
[6] R. Giering . Tangent linear and Adjoint Model Compiler, Users manual. Technical report, 1997. http://www.autodiff.com/tamc.
[6] V. Capretta . General recursion via coinductive types. Logical Methods in Computer Science, 1(2:1):1–28, 2005.
[6] Y. Bertot . Formalizing a jvml verifier for initialization in a theorem prover. In Computer Aided Verification (CAV'2001), volume 2102, Lecture Notes in Computer Science, pp. 14–24. Springer-Verlag, 2001.
[6] Y. Coscoy . A natural language explanation for formal proofs. In Logical Aspects of Computational Linguistics, LACL'96, Nancy France.
[70] D. M. Ritchie and K. Thompson . The UNIX time-sharing system. Commun. ACM, 17(7):365–375, 1974.
[70] M. Tomita . Efficient Parsing for Natural Language: A Fast Algorithm for Practical Systems. Kluwer Academic Publishers, Norwell, MA, USA, 1985.
[71] J. E. Rodriguez . A Graph Model for Parallel Computations. Technical Report TR-64, MIT Project MAC, September 1969.
[72] D. Scott . Outline of a Mathematical Theory of Computation. Technical Report Technical Monograph PRG-2, Programming Research Group, Oxford University, November 1970.
[73] D. Scott . Continuous Lattices. Technical Report Technical Monograph PRG-7, Programming Research Group, Oxford University, August 1971.
[74] D. Scott . Data types as lattices. SIAM J. Comput., 5:522–587, 1976.
[75] D. Seror . D. C. P. L: A Distributed Control Programming Language. PhD thesis, University of Utah, 1970.
[76] S. F. Smith . A computational induction principle. unpublished note, July 1991.
[77] D. A. Turner . An overview of Miranda. SIGPLAN Notices, 21, 1986.
[78] D. A. Turner . SASL Language Manual. Technical report, St. Andrews University, Department of Computational Science, December 1976.
[79] D. A. Turner . The semantic elegance of applicative languages. In Proceedings of the 1981 Conf. on Functional Programming and Computer Architecture, 1981.
[7] A. E. Ashcroft and W. W. Wadge . Lucid: Scope Structures and Defined Functions. Technical Report Rep. CS-76-22, Computer Science Dept., University of Waterloo, 1976.
[7] B. Courcelle and T. Knapik , The evaluation of first-order substitution is monadic second-order compatible. Theoretical Computer Science, 281:177–206, 2002.
[7] F. Baccelli , K. B. Kim and D. De Vleeschauwer . Analysis of the competition between wired, DSL and wireless users in an access network. In Proceedings of IEEE Infocom, Miami, FL, USA, March 2005.
[7] F. Hamelin and P. Bernhard . Uncoupling Isaacs'equations in two-player nonzero-sum differential games. Parental conflict over care as an example. Automatica, 44:882–885, 2008.
[7] G. Berry and G. Boudol . The chemical abstract machine. Theoretical Computer Science, 96:217–248, 1992.
[7] H. Curry and R. Feys . Combinatory Logic, volume 1. North-Holland, 1958.
[7] J. A. Bergstra and P. Klint . The ToolBus: a Component Interconnection Architecture. Technical Report P9408, University of Amsterdam, Programming Research Group, 1994.
[7] J. Bestel , F. Clément and M. Sorine . A biomechanical model of muscle contraction. In W. J. Niessen and M. A. Viergever (eds) Proc. of International Conference on Medical Image Computing and Computer Assisted Intervention (MICCAI'01), volume 2208, Lecture Notes in Computer Science, pp. 1159–1161. Springer-Verlag, 2001.
[7] J. Field . A simple rewriting semantics for realistic imperative programs and its application to program analysis. In PEPM, pp. 98–107, 1992.
[7] L. Théry , Y. Bertot and G. Kahn . Real theorem provers deserve real user-interfaces. ACM SIGSOFT Symposium on Software Development Environments. 1992.
[7] M. Butt , H. Dyvik , T. Holloway King , H. Masuichi and C. Rohrer . The Parallel Grammar Project. In COLING 2002, Workshop on Grammar Engineering and Evaluation, pp. 1–7, 2002.
[7] M. J. E. Stermberg and S. H. Muggleton . Structure Activity Relationships (SAR) and pharmacophore discovery using inductive logic programming (ILP). QSAR Comb. Sci. 22:527–532, 2003.
[7] P. Caspi . Clocks in dataflow languages. Theoretical Computer Science, 94(1), 1992.
[7] P. Caspi and M. Pouzet . Synchronous Kahn Networks. In ACM SIGPLAN International Conference on Functional Programming, Philadelphia, Pensylvania, May 1996.
[7] P.-L. Curien , On the symmetry of sequentiality. In Proceedings of Mathematical Foundations of Programming Semantics 1993, Lecture Notes in Computer Science 802, Springer-Verlag, pp. 29–71 (1994).
[7] R. Giering and T. Kaminski . Generating recomputations in reverse mode AD. In [3], chapter VIII, pp. 283–291. 2002.
[7] R. Milner , Models of LCF. Stanford Computer Science Department Report. CS-332, 1973.
[7] S. Brenner . Interview. Discover Magazine 25(4), 2004.
[7] V. Donzeau-Gouge , G. Huet , G. Kahn and B. Lang . Programming environments based on structured editors: The MENTOR experience, 1984.
[7] X. Leroy . Polymorphic Typing of an Algorithmic Language. PhD thesis, University Paris 7, 1992. INRIA Research Report, No 1778.
[7] Y. Bertot . A survey of semantics styles, 2007. available on the Coq site at coq.inria.fr/Semantics_survey.html.
[80] J. Vuillemin . Correct and optimal implementations of recursion in a simple programming language. In STOC '73: Proceedings of the Fifth Annual ACM Symposium on Theory of Computing, pp. 224–239, New York, NY, USA, 1973. ACM Press.
[81] J. Vuillemin . Correct and optimal implementations of recursion in a simple programming language. J. Comput. System Sci., 9(3):332–354, December 1974.
[82] C. P. Wadsworth . Semantics and Pragmatics of the Lambda-calculus. PhD thesis, Oxford University, 1971.
[83] Z. Wan and P. Hudak . Functional Reactive Programming from first principles. In Proceedings of the ACM SIGPLAN'00 Conference on Programming Language Design and Implementation (PLDI'00), 2000.
[84] E. Wiedmer . Exaktes rechnen mit reellen zahlen. Technical Report Bericht no. 20, Eidgenössische Technische Hocchschule, Zurich, July 1976.
[85] G. Winskel . Events in Computation. PhD thesis, Edinburgh University, 1981.
[8] A. Cohen , M. Duranton , C. Eisenbeis , C. Pagetti , F. Plateau and M. Pouzet . N-Synchronous Kahn networks: a relaxed model of synchrony for real-time systems. In ACM International Conference on Principles of Programming Languages (POPL'06), Charleston, South Carolina, USA, January 2006.
[8] A. E. Ashcroft and W. W. Wadge . Lucid, a nonprocedural language with iteration. Commun. ACM, 20(7):519–526, 1977.
[8] A. Griewank . Evaluating Derivatives: Principles and Techniques of Algorithmic Differentiation. SIAM, Frontiers in Applied Mathematics, 2000.
[8] A. I. Houston and N. B. Davies . The evolution of cooperation and life history in the dunnock Prunella modularis. In Behavioural Ecology, R. M. Silby and R. H. Smith (eds) pp. 471–487. Blackwell Scientific Publications, 1985.
[8] B. Courcelle and J. Vuillemin , Completeness results for the equivalence of recursive schemas. Journal of Computing Systems Science, 12:179–197, 1976.
[8] C.-H. Yuh , H. Bolouri and E. H. Davidson . Genomic cis-regulatory logic: experimental and computational analysis of a sea urchin. Gene. Science, 279:1896–1902, 1998.
[8] Eclipse homepage . www.eclipse.org.
[8] F. Baccelli , D. McDonald and J. Reynier . A mean-field model for multiple TCP connections through a buffer implementing RED. Performance Evaluation, No. 11, 77–97, 2002.
[8] H. Curry , R. Feys and J. Seldin . Combinatory Logic, volume 2. North-Holland, 1972.
[8] J. A. Bergstra and P. Klint . The discrete time ToolBus – a software coordination architecture. Science of Computer Programming, 31(2–3):205–229, 1998.
[8] J. Boisvert , X. Pennec , H. Labelle , F. Cheriet and N. Ayache . Principal spine shape deformation modes using Riemannian geometry and articulated models. In Proc. of the IV Conference on Articulated Motion and Deformable Objects, Andratx, Mallorca, Spain, 11–14 July, volume 4069, Lecture Notes in Computer Science, pp. 346–355. Springer-Verlag, 2006. AMDO best paper award 2006.
[8] M. Creeger . Multicore CPUs for the masses. ACM Queue, 3(7):63–64, 2005.
[8] N. Carriero and D. Gelernter . Linda in Context. Communications of the ACM, 32(4):444–458, 1989.
[8] O. Caprotti . WebALT! Deliver Mathematics Everywhere. In Proceedings of SITE 2006. Orlando March 20–24, 2006.
[8] P.-L. Curien , Introduction to Linerar logic and ludics, parts I and II, Advances of Mathematics (China) 34(5):513–544 (2005) and 35(1):1–44 (2006).
[8] R. Giacobazzi and I. Mastroeni . Non-standard semantics for program slicing. HOSC, 16(4):297–339, 2003.
[8] R. Milner . A theory of type polymorphism in programming. Journal of Computer Systems Science, 17:348–375, 1978.
[8] R. Milner and R. Weyrauch , Proving compiler correctness in a mechanized logic. In B. Meltzer and D. Michie (eds), Machine Intelligence 7, pp. 51–72. Edinburgh University Press, 1972.
[8] S. H. Muggleton , H. Lodhi , A. Amini and M. J. E. Sternberg . Support vector inductive logic programming. In Proc. 8th International Conference on Discovery Science, volume 3735, Lecture Notes in Artificial Intelligence, pp. 163–175. Springer Verlag, 2005.
[8] Y. Bertot , G. Kahn and L. Théry . Proof by pointing. In M. Hagiya and J. C. Mitchell (eds), Proceedings of the International Symposium on Theoretical Aspects of Computer Software. volume 789, Lecture Notes in Computer Science, Sendai, Japan, p 141–160, Springer-Verlag, 1994.
[8] Y. Bertot and P. Castéran . Interactive Theorem Proving and Program Development, Coq'Art:the Calculus of Inductive Constructions. Springer-Verlag, 2004.
[9] A. Bakre and B. R. Badrinath . I-TCP: Indirect TCP for Mobile Hosts. Proceedings of the 15th ICDCS, May 1995.
[9] A. E. Ashcroft and W. W. Wadge . Structured Lucid. Technical Report CS-79-21, Computer Science Department, University of Waterloo, 1979.
[9] A. I. Houston , T. Szekely and J. M. McNamara . Conflict between parents over care. Trends in Ecology and Evolution, 20:33–38, 2005.
[9] A. Wagner . How to reconstruct a large genetic network from n gene perturbations in fewer than n easy steps. Bioinformatics, 17(12):1183–1197, 2001.
[9] B. A. Davey and H. A. Priestley . Introduction to Lattices and Order. Cambridge University Press, 1990.
[9] B. Courcelle , G. Kahn and J. Vuillemin . Algorithmes d'équivalence et de réduction à des expressions minimales dans une classe d'équations récursives simples. In J. Loeckx (ed.) Automata, Languages and Programming, volume 14, Lecture Notes in Computer Science, pp. 200–213. Springer-Verlag, 1974. Translation from French by T. Veldhuizen with original text, a few comments and additional references.
[9] D. Chapelle , F. Clément , F. Génot , P. Le Tallec , M. Sorine and J. Urquiza . A physiologically-based model for the active cardiac muscle contraction. In T. Katila , I. E. Magnin , P. Clarysse , J. Montagnat and J. Nenonen (eds) Functional Imaging and Modeling of the Heart (FIMH'01), Helsinki, Finland, volume 2230, Lecture Notes in Computer Science. Springer-Verlag, 2001.
[9] I. Guessarian , Algebraic Semantics, Lecture Notes in Computer Science 99, Springer Verlag, 1981.
[9] J. Hatcliff , J. Corbett , M. Dwyer , S. Sokolowski and H. Zheng . A formal study of slicing for multi-threaded programs with JVM concurrency primitives. In SAS, 1999.
[9] J. M. Zytkow , J. Zhu and A. Hussam . Automated discovery in a chemistry laboratory. In Proc. 8th National Conference on Artificial Intelligence, Boston, MA, USA, pp. 889–894, AAAI Press, MIT Press, 1990.
[9] K. Mani Chandy and J. Misra . Parallel Program Design : A Foundation. Addison-Wesley, 1988.
[9] L. Damas and R. Milner . Principal type-schemes for functional programs. In POPL, pp. 207–212, 1982.
[9] L. Hascoët . The Data-dependence Graph of Adjoint Programs. Research Report 4167, INRIA, 2001.
[9] M. Nivat , Sur l'interprétation des schémas de programmes monadiques. Rapport Laboria No. 1, 1972.
[9] P.-L. Curien , Combinateurs Catégoriques, Algorithmes Séquentiels et Programmation Fonctionnelle, Thèse d'Etat, Université Paris 7 (1983); English version: Categorical Combinators, Sequential Algorithms and Functional Programming, Research Notes in Theoretical Computer Science, Pitman (1986); second, revised edition, Birkhaüser (1993).
[9] T. Hallgren . Alfa homepage. www.cs.chalmers.se/∼hallgren/Alfa/, 1996–2000.
[9] W. Naraschewski and T. Nipkow . Type inference verified: Algorithm W in Isabelle/HOL. Journal of Automated Reasoning, 23:299–318, 1999.
[9] Y. Bertot . Implementation of an interpreter for a parallel language in Centaur. In European Symposium on Programming, pp. 57–69, 1990.
[9] Y. Bertot and R. Fraer . Reasoning with executable specifications. In TAPSOFT'95, volume 915, Lecture Notes in Computer Science, pp. 531–545, 1995.
[9] Y. Coscoy . Explication textuelle de preuves pour le calcul des constructions inductives. PhD thesis, Université de Nice-Sophia-Antipolis, 2000.
[9]The Calculus of Constructions. Documentation and User's Guide, Version 4.10. Technical Report 110, INRIA, 1989.
The Coq Development Team . The Coq Proof Assistant Reference Manual – Version V8.1, July 2006. http://coq.inria.fr.