From Semantics to Computer Science

Essays in Honour of Gilles Kahn

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.

Reference Title: References

Reference Type: bibliography

[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.
[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.
[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.
[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.
[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.
[6] J.-P. Banâtre and D. Le Métayer . Programming by multiset transformation. Communications of the ACM (CACM), 36(1):98–111, 1993.
[7] G. Berry and G. Boudol . The chemical abstract machine. Theoretical Computer Science, 96:217–248, 1992.
[8] N. Carriero and D. Gelernter . Linda in Context. Communications of the ACM, 32(4):444–458, 1989.
[9] K. Mani Chandy and J. Misra . Parallel Program Design : A Foundation. Addison-Wesley, 1988.
[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.
[11] C. A. R. Hoare . Communicating sequential processes. Communications of the ACM, 21(8):666–677, 1978.
[12] G. Kahn . The semantics of a simple language for parallel programming. Information Processing, 74:471–475, 1974.
[13] R. Milner . A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer-Verlag, 1980.
[14] T. Murata . Petri nets: Properties, analysis and applications. Proceedings of the IEEE, 77(4):541–580, 1989.
[15] H. R. Barradas . Une approche à la dérivation formelle de systèmes en Gamma. PhD thesis, Université de Rennes 1, France, 1993.

Reference Title: References

Reference Type: bibliography

[1] R. Amadio and P.-L. Curien , Domains and Lambda-calculi, Cambridge University Press (1998).
[2] G. Berry , Stable models of typed lambda-calculi. In Proc. ICALP 1978, Lecture Notes in Computer Science 62 Springer-Verlag (1978).
[3] G. Berry and P.-L. Curien , Sequential algorithms on concrete data structures, Theoretical Computer Science 20:265–321 (1982).
[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).
[5] R. Cartwright and M. Felleisen , Observable sequentiality and full abstraction. In Proc. POPL 1992 (1992).
[6] R. Cartwright , P.-L. Curien and M. Felleisen , Fully abstract semantics for observably sequential languages, Information and Computation 111(2):297–401 (1994).
[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).
[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).
[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).
[10] P.-L. Curien , Symmetry and interactivity in programming, Bulletin of Symbolic Logic 9(2):169–180 (2003).
[11] J.-Y. Girard , Linear logic, Theoretical Computer Sciences 50:1–102 (1987).
[12] J.-Y. Girard , Locus Solum, Mathematical Structures in Computer Science (2001).
[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).
[14] G. Kahn and G. Plotkin , Concrete domains, Theoretical Computer Science 12:187–277 (1993).
[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).
[16] J. Laird , Locally boolean domains, Theoretical Computer Science 342:132–248 (2005).
[17] F. Lamarche , Sequentiality, games and linear logic. In Proc. CLICS Workshop, Aarhus University, DAIMI-397-II (1992).
[18] T. Loew , Locally Boolean Domains and Universal Models for Infinitary Sequential Languages, PhD Thesis, Technische Universität Darmstadt (2006).
[19] T. Streicher , Laird domains, draft (2002).

Reference Title: References

Reference Type: bibliography

[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.
[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.
[3] G. Berry . Bottom-up computation of recursive programs. Revue Française d'Automatique, Informatique et Recherche Opérationnelle, 10(3):47–82, 1976.
[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.
[5] M. Broy . Functional specification of time-sensitive communicating systems. ACM Transactions on Software Engineering and Methodology, 2(1):1–46, 1993.
[6] M. Broy and G. Stefanescu . The algebra of stream processing functions. Theoretical Computer Science, 258:99–129, 2001.
[7] P. Caspi . Clocks in dataflow languages. Theoretical Computer Science, 94(1), 1992.
[8] M. Creeger . Multicore CPUs for the masses. ACM Queue, 3(7):63–64, 2005.
[9] B. A. Davey and H. A. Priestley . Introduction to Lattices and Order. Cambridge University Press, 1990.
[10] J. B. Dennis . First Version Data Flow Procedure Language. Technical Report MAC TM61, MIT Laboratory for Computer Science, 1974.
[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.
[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.
[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.
[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] G. Kahn . The semantics of a simple language for parallel programming. In Proc. of the IFIP Congress 74. North-Holland Publishing Co., 1974.
[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.
[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.
[18] E. A. Lee and T. M. Parks . Dataflow process networks. Proceedings of the IEEE, 83(5):773–801, 1995.
[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.
[20] S. G. Matthews . An extensional treatment of lazy data flow deadlock. Theoretical Computer Science, 151(1):195–205, 1995.
[21] A. G. Olson and B. L. Evans . Deadlock detection for distributed process networks. In ICASSP, 2005.
[22] O. M. G. (OMG) . A UML profile for MARTE, beta 1. OMG Adopted Specification ptc/07–08–04, August 2007.
[23] T. M. Parks . Bounded Scheduling of Process Networks. PhD, UC Berkeley, 1995.
[24] T. M. Parks and D. Roberts . Distributed process networks in Java. In International Parallel and Distributed Processing Symposium, Nice, France, April 2003.
[25] D. Scott . Outline of a mathematical theory of computation. In 4th Annual Princeton Conference on Information Sciences and Systems, pp. 169–176, 1970.
[26] V. Srini . An architectural comparison of dataflow systems. Computer, 19(3), 1986.
[27] E. W. Stark . An algebra of dataflow networks. Fundamenta Informaticae, 22(1–2):167–185, 1995.
[28] R. Stephens . A survey of stream processing. Acta Informatica, 34(7), 1997.
[29] C. L. Talcott . Interaction semantics for components of distributed systems. In Formal Methods for Open Object-Based Distributed Systems (FMOODS), 1996.
[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.
[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.
[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.

Reference Title: References

Reference Type: bibliography

[1] H. Abelson , G. J. Sussman , and J. Sussman . Structure and Interpretation of Computer Programs. McGraw-Hill, New York, 1985.
[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.
[3] D. A. Adams . A Computation Model with Data Flow Sequencing. PhD thesis, Computer Science Dept, Stanford University, December 1968. Technical Report CS-117.
[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.
[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.
[6] A. E. Ashcroft and W. W. Wadge . Lucid – a formal system for writing and proving programs. SIAM J. Comput., 5:519–526, 1976.
[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.
[8] A. E. Ashcroft and W. W. Wadge . Lucid, a nonprocedural language with iteration. Commun. ACM, 20(7):519–526, 1977.
[9] A. E. Ashcroft and W. W. Wadge . Structured Lucid. Technical Report CS-79-21, Computer Science Department, University of Waterloo, 1979.
[10] A. E. Ashcroft and W. W. Wadge . Lucid, the Dataflow Programming Language. Number 22 in APIC Studies in Data Processing. Academic Press, 1985.
[11] J. L. Baer . A survey of some theoretical aspects of multiprocessing. ACM Comput. Surv., 5(1):31–80, 1973.
[12] G. Berry and P.-L. Currien . Sequential algorithms on concrete data structures. Theoret. Comput. Sci., 20:265–322, 1982.
[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.
[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.
[15] S. Brookes . Historical introduction to “concrete domains” by G. Kahn and G. D. Plotkin. Theoret. Comput. Sci., 121(1–2):179–186, 1993.
[16] W. H. Burge . Recursive Programming Techniques. Addison Wesley, 1975.
[17] W. H. Burge . Stream processing functions. IBM J. Res. Develop., pp. 12–25, 1975.
[18] R. M. Burstall . Design considerations for a functional programming language. In Infotech State of the Art Conference: The Software Revolution, Copenhagen, October 1977.
[19] R. M. Burstall , J. S. Collins , and R. J. Popplestone . Programming in POP-2. Edinburgh University Press, 1977.
[20] R. M. Burstall and J. Darlington . A tranformation system for developing recursive programs. J. ACM, 24(1), 1977.
[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.
[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.
[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.
[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.
[25] M. E. Conway . Design of a separable transition-diagram compiler. Commun. ACM, 6(7):396–408, 1963.
[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.
[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.
[28] J. Davies . POP-10 User's Manual. Technical Report CS R25, University of Western Ontario Computer Science Dept., 1976.
[29] J. B. Dennis . Programming generality, parallelism, and computer architecture. In Information Processing 68, pp. 484–492. North Holland, 1969.
[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.
[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.
[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.
[33] J. B. Dennis . Stream Data Types for Signal Processing. Computation Structures Group Memo 36, MIT LCS, October 1994.
[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] 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.
[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.
[37] J. R. Gurd , C. C. Kirkham and I. Watson . The Manchester prototype dataflow computer. Commun. ACM, 28(1):34–52, 1985.
[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.
[39] E. Harold . Java I/O, 2nd Edition. O'Reilly Media, 2006.
[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.
[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.
[42] G. Kahn and G. D. Plotkin . Domaines concrets. INRIA Rapport 336, INRIA, 1978.
[43] G. Kahn and G. D. Plotkin . Concrete domains. Theoret. Comput. Sci., 121(1–2):187–277, 1993.
[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.
[45] G. Kahn . A Preliminary Theory for Parallel Programs. Technical Report Rapport Laboria no. 6, IRIA Rocquencourt, January 1973.
[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.
[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 and G. Plotkin . Concrete Data-types. first draft manuscript, December 1975.
[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.
[50] J. Kelly , C. Lochbaum and V. Vyssotsky . A block diagram compiler. Bell System Tech. J., 40(3):669–676, May 1961.
[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.
[53] P. J. Landin . A correspondence between ALGOL 60 and Church's lambda-notation: Part I. Commun. ACM, 8(2):89–101, 1965.
[54] D. C. Luckham , D. M. R. Park and M. S. Paterson . On formalized computer programs. J. System Sci., 4(3):220–249, 1970.
[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.
[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.
[57] J. McCarthy . Towards a mathematical science of computation. In Proceedings of the IFIP Congress 1962, pp. 21–28. North-Holland, 1962.
[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] M. D. McIlroy . Coroutines. unpublished note, May 1968.
[60] M. D. McIlroy . Squinting at power series. Software Pract. Exper., 20:661–683, 1990.
[61] M. D. McIlroy . Power Series as Lazy Streams. Technical Report BL011276-970313-02TMS, Bell Laboratories, Lucent Technologies, 1997.
[62] M. D. McIlroy . Power series, power serious. J. Funct. Program., 9(3):325–337, May 1999.
[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] R. Milner . Processes: A mathematical model of computing agents. In Proceedings of the Colloquium in Mathematical Logic, pp. 157–173. North-Holland, 1973.
[65] R. Milner and R. Weyrauch . Proving compiler correctness in a mechanized logic. In Machine Intelligence 7. Edinburgh University Press, 1972.
[66] S. Peyton-Jones (ed.) Haskell98, Languages and Libraries, The Revised Report. Cambridge University Press, 2003.
[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.
[69] D. M. Ritchie . A stream input-output system. AT&T Bell Laboratories Tech. J., 63(8):1897–1910, 1984.
[70] D. M. Ritchie and K. Thompson . The UNIX time-sharing system. Commun. ACM, 17(7):365–375, 1974.
[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.
[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.

Reference Title: References

Reference Type: bibliography

[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.
[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.
[3] A. Colmerauer , Prolog and infinite trees, logic programming, In: W. Clark and S. Tarnlund (eds.), pp. 153–172. Academic Press, 1982.
[4] B. Courcelle , Fundamental properties of infinite trees, Theoretical Computer Science, 25:95–169, 1983.
[5] B. Courcelle , Equivalences and transformations of regular systems. Applications to recursive program schemes and grammars. Theoretical Computer Science, 42:1–122, 1986.
[6] B. Courcelle , Recursive applicative program schemes. In: J. Van Leeuwen (ed.), Handbook of Theoretical Computer Science, Volume B, pp. 459–492. Elsevier, 1990.
[7] B. Courcelle and T. Knapik , The evaluation of first-order substitution is monadic second-order compatible. Theoretical Computer Science, 281:177–206, 2002.
[8] B. Courcelle and J. Vuillemin , Completeness results for the equivalence of recursive schemas. Journal of Computing Systems Science, 12:179–197, 1976.
[9] I. Guessarian , Algebraic Semantics, Lecture Notes in Computer Science 99, Springer Verlag, 1981.
[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.
[11] G. Huet , Résolution d'équations dans des langages d'ordre 1, 2, …, ω. Doctoral dissertation, Université Paris 7, 1976.
[12] P. Mosses , Denotational semantics. In: J. Van Leeuwen (ed.), Handbook of Theoretical Computer Science, Volume B, pp. 575–632. Elsevier, 1990.
[13] M. Rabin , Decidability of second-order theories and automata on infinite trees, Transactions of the American Mathematical Society, 141:1–35, 1969.
[14] G. Sénizergues , Complete formal systems for equivalence problems, Theoretical Computer Science, 231:309–334, 1999.
[15] G. Sénizergues , L(A) = L(B)?, Theoretical Computer Science, 251:1–166, 2001.
[16] I. Walukiewicz , Completeness of Kozen's axiomatization of propositional µ-calculus, Information and Computation, 157:142–182, 2000.

Reference Title: References

Reference Type: bibliography

[1] B. Courcelle and J. Vuillemin , Completeness results for the equivalence of recursive schemes, Journal of Computer System Science 12:179–197, 1976.
[2] W.P. De Roever , Operational and mathematical semantics for first-order recursive program schemas, (private communication).
[3] J. Engelfriet , A note on infinite trees, Information Processing Letters 1:229–232, 1972.
[4] G. Kahn , A preliminary theory for parallel programs. (Rapport Laboria no. 6, January 1973).
[5] J. Kral , Equivalence of modes and the equivalence of finite automata, Algol Bulletin 35:34–35, 1973.
[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.
[7] R. Milner , Models of LCF. Stanford Computer Science Department Report. CS-332, 1973.
[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.
[9] M. Nivat , Sur l'interprétation des schémas de programmes monadiques. Rapport Laboria No. 1, 1972.
[10] C. Pair , Concerning the syntax of Algol 68, Algol Bulletin 31:16–27, 1970.
[11] D. Scott , Outline of a Mathematical Theory of Computation. Oxford Monograph PRG-2. Oxford University, 1970.
[12] J. Vuillemin , Proof Techniques for Recursive Programs. PhD thesis, Stanford Computer Science Department. 1973.

Reference Title: References

Reference Type: bibliography

[1] R. Amadio and P.-L. Curien. Domains and Lambda-calculi. Cambridge University Press, 1998.
[2] H. Barendregt . Handbook of Mathematical Logic, chapter the type free lambda calculus. In North-Holland, 1977.
[3] H. Barendregt . The Lambda Calculus, Its Syntax and Semantics. North-Holland, 1984.
[4] G. Berry and J.-J. Lévy . Minimal and optimal computations of recursive programs. JACM, 26(1):148–175, January 1979.
[5] G. Boudol . Computational semantics of term rewriting systems. In Algebraic methods in Semantics. Cambridge University Press, 1985.
[6] A. Church . The Calculi of Lambda-Conversion. Princeton University Press – Oxford University Press, 1941.
[7] H. Curry and R. Feys . Combinatory Logic, volume 1. North-Holland, 1958.
[8] H. Curry , R. Feys and J. Seldin . Combinatory Logic, volume 2. North-Holland, 1972.
[9] L. Damas and R. Milner . Principal type-schemes for functional programs. In POPL, pp. 207–212, 1982.
[10] R. Hindley . Basic Simple Type Theory. Cambridge University Press, 1997.
[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.
[12] J.-W. Klop . Combinatory Reduction Systems. PhD thesis. Mathematical Centre Tracts 127, CWI, Amsterdam, 1980.
[13] P. Landin . A correspondence between Algol 60 and Church's lambda-notation. CACM, 8(2):89–101, 1965.
[14] C. Laneve . Distributive evaluations of lambda-calculus. Fundamenta Informaticae, 20(4):333–352, 1994.
[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.
[16] J.-J. Lévy . Réductions correctes et optimales dans le lambda calcul. PhD thesis, University of Paris 7, 1978. (in French).
[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.
[18] L. Maranget . La stratégie paresseuse. PhD thesis, University of Paris 7, July 1992.
[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.
[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.
[21] V. V. Oostrom and R. D. Vrijer . Equivalence of reductions. In Terese, Term Rewriting Systems. Cambridge University Press, March 2003.
[22] G. Plotkin . Call-by-name, call-by-value, and the lambda-calculus. Theoretical Computer Science, 1, 1975.
[23] D. van Daalen . The Language Theory of Automath. PhD thesis, TUE, 1980.
[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] V. van Oostrom and R. de Vrijer . Four equivalent equivalences of reductions. In WRS'02, volume 70(6), ENTCS, December 2002.
[26] G. Winskel . Event structure semantics for ccs and related languages. Technical report, DAIMI – AARhus University, April 1983.

Reference Title: References

Reference Type: bibliography

[1] A. Aho , R. Sethi and J. Ullman . Compilers: Principles, Techniques and Tools. Addison-Wesley, 1985.
[2] B. Alpern , M. Wegman , and F. Zadeck . Detecting equality of variables in programs. In POPL, pp. 1–11, 1988.
[3] T. Amtoft . Slicing for modern program structures: a theory for eliminating irrelevant loops. Information Processing Letters, 106:45–51, 2008.
[4] R. Cartwright and M. Felleisen . The semantics of program dependence. In PLDI, pp. 13–27, 1989.
[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.
[6] J. Ferrante , K. Ottenstein and J. Warren . The program dependence graph and its use in optimization. TOPLAS, 3(9):319–349, 1987.
[7] J. Field . A simple rewriting semantics for realistic imperative programs and its application to program analysis. In PEPM, pp. 98–107, 1992.
[8] R. Giacobazzi and I. Mastroeni . Non-standard semantics for program slicing. HOSC, 16(4):297–339, 2003.
[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.
[10] S. Horwitz , J. Prins and T. Reps . On the adequacy of program dependence graphs for representing programs. In POPL, pp. 146–157, 1988.
[11] S. Horwitz , J. Prins and T. Reps . Integrating non-interfering versions of programs. TOPLAS, 11(3):345–387, 1989.
[12] G. Kahn . The semantics of simple language for parallel programming. In IFIP Congress, pp. 471–475, 1974.
[13] D. Kuck , R. Kuhn , B. Leasure , D. Padua and M. Wolfe . Dependence graphs and compiler optimizations. In POPL, pp. 207–218, 1981.
[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.
[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.
[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.
[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.
[18] G. Ramalingam and T. Reps . Appendix A: Proofs. “www.cs.wisc.edu/wpis/papers/soprgs08-proofs.pdf”.
[19] G. Ramalingam and T. Reps . Semantics of program representation graphs. TR-900, Computer Science Department, University of Wisconsin, Madison, WI, 1989.
[20] T. Reps and W. Yang . The semantics of program slicing and program integration. In CCIPL, pp. 360–374, 1989.
[21] B. Rosen , M. Wegman , and F. Zadeck . Global value numbers and redundant computations. In POPL, pp. 12–27, 1988.
[22] R. Selke . A rewriting semantics for program dependence graphs. In POPL, pp. 12–24, 1989.
[23] R. Shapiro and H. Saint . The representation of algorithms. Tech. Rep. CA-7002-1432, Massachusetts Computer Associates, 1970.
[24] D. Weise , R. Crew , M. Ernst and B. Steensgaard . Value dependence graphs: Representation without taxation. In POPL, pp. 297–310, 1994.
[25] M. Weiser . Program slicing. In ICSE, pp. 439–449, 1981.
[26] W. Yang . A New Algorithm for Semantics-Based Program Integration. PhD thesis, Computer Science Department, University of Wisconsin, Madison, WI, Aug. 1990.
[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] W. Yang , S. Horwitz and T. Reps . A program integration algorithm that accommodates semantics-preserving transformations. TOSEM, 1(3):310–354, July 1992.

Reference Title: References

Reference Type: bibliography

[1] I. Attali . A natural semantics for Eiffel dynamic binding. ACM Transactions on Programming Languages and Systems (TOPLAS), 18(5), 1996.
[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.
[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.
[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.
[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.
[6] J. A. Bergstra , J. Heering and P. Klint (eds), Algebraic Specification. ACM Press/Addison-Wesley, 1989.
[7] J. A. Bergstra and P. Klint . The ToolBus: a Component Interconnection Architecture. Technical Report P9408, University of Amsterdam, Programming Research Group, 1994.
[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.
[9] Y. Bertot . Implementation of an interpreter for a parallel language in Centaur. In European Symposium on Programming, pp. 57–69, 1990.
[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.
[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] 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] S. Billot and B. Lang . The structure of shared forests in ambiguous parsing. In ACL, pp. 143–151, 1989.
[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.
[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.
[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.
[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.
[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.
[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.
[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.
[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.
[22] Centaur web pp. , Last visit December 2006. http://www-sop.inria.fr/croap/centaur/centaur.html.
[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.
[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.
[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.
[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.
[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.
[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.
[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.
[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.
[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] J. Coutaz . The Box, a Layout Abstraction for User Interface Toolkits. Technical Report CMU-CS-84-167, Carnegie Mellon University, 1984.
[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.
[35] A. van Deursen , P. Klint and F. Tip . Origin tracking. Journal of Symbolic Computing 15(5–6):523–545, 1993.
[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] 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] 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] 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.
[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] 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.
[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.
[43] J. Heering and P. Klint . Towards monolingual programming environments. ACM Transactions on Programming Languages and Systems, 7(2):183–213, April 1985.
[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.
[45] J. Heering , P. Klint and J. Rekers . Incremental generation of parsers. IEEE Transactions on Software Engineering, 16(12):1344–1350, 1990.
[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.
[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.
[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.
[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.
[51] G. Kahn and D. B. MacQueen . Coroutines and networks of parallel processes. In IFIP Congress, pp. 993–998, 1977.
[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. Klint . Formal language definitions can be made practical. In Algorithmic Languages, pp. 115–132, 1981.
[54] P. Klint . A Survey of Three Language-independent Programming Environments. RR 257, INRIA, 1983.
[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] P. Klint . A meta-environment for generating programming environments. ACM Transactions on Software Engineering and Methodology, 2(2):176–201, April 1993.
[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.
[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.
[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.
[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.
[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.
[63] Meta-Environment web pp. , Last visit March 2008. http://www.meta-environment.org.
[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.
[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.
[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.
[67] D. C. Oppen . Prettyprinting. ACM Transactions on Programming Languages and Systems, 2(4):465–483, 1980.
[68] Sophtalk web pp. , Last visit December 2006. http://www-sop.inria.fr/croap/sophtalk/sophtalk.html.
[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.
[70] M. Tomita . Efficient Parsing for Natural Language: A Fast Algorithm for Practical Systems. Kluwer Academic Publishers, Norwell, MA, USA, 1985.

Reference Title: References

Reference Type: bibliography

[1] Agda homepage . unit.aist.go.jp/cvs/Agda/.
[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.
[3] R. Bornat and B. Sufrin . Animating formal proof at the surface: The Jape proof calculator. Computer Journal, 42(3):177–192, 1999.
[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.
[5] Coq homepage . pauillac.inria.fr/coq/, 1999.
[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.
[7] V. Donzeau-Gouge , G. Huet , G. Kahn and B. Lang . Programming environments based on structured editors: The MENTOR experience, 1984.
[8] Eclipse homepage . www.eclipse.org.
[9] T. Hallgren . Alfa homepage. www.cs.chalmers.se/∼hallgren/Alfa/, 1996–2000.
[10] J. Harrison . The HOL light theorem prover. www.cl.cam.ac.uk/∼jrh13/hol–light/, 2006.
[11] G. Huet and G. Plotkin (eds) Logical Frameworks: First International Workshop on Logical Frameworks, Antibes, May, 1990. Cambridge University Press, 1991.
[12] G. Huet and G. Plotkin (eds) Logical Environments: Second International Workshop on Logical Frameworks, Edinburgh, May, 1991. Cambridge University Press, 1993.
[13] Isabelle Homepage . www.cl.cam.ac.uk/Research/HVG/Isabelle/, 2003.
[14] D. E. Knuth . Literate Programming. CSLI, 1992.
[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.
[16] P. Martin-Löf . Intuitionistic Type Theory. Bibliopolis, Napoli, 1984.
[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.
[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.
[19] R. Pollack . The LEGO proof assistant. www.dcs.ed.ac.uk/home/lego/, 1997.
[20] A. Ranta . Grammatical Framework Homepage. www.cs.chalmers.se/∼aarne/GF/, 1999–2005.
[21] A. Ranta . Grammatical Framework: A Type-Theoretical Grammar Formalism. Journal of Functional Programming, 14(2):145–189, 2004.
[22] The Types Project Homepage . www.cs.chalmers.se/Cs/Research/Logic/Types/.
[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.

Reference Title: References

Reference Type: bibliography

[1] A. Appel . Modern Compiler Implementation in Java. Cambridge University Press, 1998.
[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.
[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.
[4] Bescherelle . La conjugaison pour tous. Hatier, 1997.
[5] B. Bringert . Embedded Grammars. MSc Thesis, Department of Computing Science, Chalmers University of Technology, 2004.
[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.
[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.
[8] O. Caprotti . WebALT! Deliver Mathematics Everywhere. In Proceedings of SITE 2006. Orlando March 20–24, 2006.
[9] Y. Coscoy . Explication textuelle de preuves pour le calcul des constructions inductives. PhD thesis, Université de Nice-Sophia-Antipolis, 2000.
[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] 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.
[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.
[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.
[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.
[15] M. Forsberg and A. Ranta . Functional Morphology. In ICFP 2004, Showbird, Utah, pp. 213–223, 2004.
[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.
[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.
[18] M. Humayoun . Urdu Morphology, Orthography and Lexicon Extraction. MSc Thesis, Department of Computing Science, Chalmers University of Technology, 2006.
[19] J. Khegai . GF parallel resource grammars and Russian. In Coling/ACL 2006, pp. 475–482, 2006.
[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.
[21] R. Montague . Formal Philosophy. Yale University Press, New Haven, 1974. Collected papers edited by R. Thomason.
[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.
[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.
[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.
[25] A. Ranta . Grammatical framework: a type-theoretical grammar formalism. Journal of Functional Programming, 14(2):145–189, 2004.
[26] A. Ranta . Modular grammar engineering in GF. Research on Language and Computation, 5:133–158, 2007.
[27] A. Ranta . Grammatical Framework Homepage, 2008. digitalgrammars.com/gf.
[28] M. Rayner , D. Carter , P. Bouillon , V. Digalakis and M. Wirén . The Spoken Language Translator. Cambridge University Press, Cambridge, 2000.
[29] B. Stroustrup . The C++ Programming Language, Third Edition. Addison-Wesley, 1998.
[30] The Coq Development Team . The Coq Proof Assistant Reference Manual. pauillac.inria.fr/coq/, 1999.
[31] A. Trybulec . The Mizar Homepage. http://mizar.org/, 2006.
[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] F. Wiedijk . Formal proof sketches. In Types for Proofs and Programs, volume 3085 Lecture Notes in Computer Science, pp. 378–393. Springer, 2004.

Reference Title: References

Reference Type: bibliography

[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.
[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.
[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.
[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.
[5] Y. Bertot . A Certified Compiler for an Imperative Language. Research Report RR-3488, INRIA, 1998.
[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.
[7] Y. Bertot . A survey of semantics styles, 2007. available on the Coq site at coq.inria.fr/Semantics_survey.html.
[8] Y. Bertot and P. Castéran . Interactive Theorem Proving and Program Development, Coq'Art:the Calculus of Inductive Constructions. Springer-Verlag, 2004.
[9] Y. Bertot and R. Fraer . Reasoning with executable specifications. In TAPSOFT'95, volume 915, Lecture Notes in Computer Science, pp. 531–545, 1995.
[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.
[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.
[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.
[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.
[14] C. Coquand . Agda. www.cs.chalmers.se/∼catarina/agda.
[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.
[16] E. W. Dijkstra . A discipline of Programming. Prentice Hall, 1976.
[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.
[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.
[19] M. J. C. Gordon and T. F. Melham . Introduction to HOL : a theorem-proving environment for higher-order logic. Cambridge University Press, 1993.
[20] M. J. C. Gordon , R. Milner and C. P. Wadsworth . Edinburgh LCF, volume 78, Lecture Notes in Computer Science. Springer-Verlag, 1979.
[21] C. A. R. Hoare . An axiomatic basis for computer programming. Communications of the ACM, 12:576–580, 1969.
[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).
[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.
[24] O. Müller , T. Nipkow , D. von Oheimb and O. Slotosch . HOLCF = HOL + LCF. Journal of Functional Programming, 9:191–223, 1999.
[25] T. Nipkow . Winskel is (almost) right: Towards a mechanized semantics. Formal Asp. Computing, 10(2):171–186, 1998.
[26] L. C. Paulson and T. Nipkow . Isabelle : a Generic Theorem Prover, volume 828, Lecture Notes in Computer Science. Springer-Verlag, 1994.
[27] D. Pichardie . Interprétation abstraite en logique intuitionniste : extraction d'analyseurs Java certifiés. PhD thesis, Université Rennes 1, 2005. (In French).
[28] G. Plotkin . Structural operational semantics. Lecture notes DAIMI FN-19, Aarhus University, 1981. (reprinted 1991).
[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.
[30] J. van den Berg and B. Jacobs . The loop compiler for Java and JML. In TACAS 2001, pp. 299–312. Springer-Verlag, 2001.
[31] D. von Oheimb . Analyzing Java in Isabelle/HOL, Formalization, Type Safety, and Hoare Logic. PhD thesis, Technische Universität München, 2000.
[32] G. Winskel . The Formal Semantics of Programming Languages, an introduction. Foundations of Computing. The MIT Press, 1993.

Reference Title: References

Reference Type: bibliography

[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.
[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.
[3] L. Damas . Type Assignment in Programming Languages. PhD thesis, University of Edinburgh, 1984.
[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.
[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.
[6] C. A. Gunter . Semantics of Programming Languages. MIT Press, 1992.
[7] X. Leroy . Polymorphic Typing of an Algorithmic Language. PhD thesis, University Paris 7, 1992. INRIA Research Report, No 1778.
[8] R. Milner . A theory of type polymorphism in programming. Journal of Computer Systems Science, 17:348–375, 1978.
[9] W. Naraschewski and T. Nipkow . Type inference verified: Algorithm W in Isabelle/HOL. Journal of Automated Reasoning, 23:299–318, 1999.
[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.
[11] A. M. Pitts . Nominal logic, A first order theory of names and binding. Information and Computation, 186:165–193, 2003.
[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.
[13] M. Tofte . Operational Semantics and Polymorphic Type Inference. PhD thesis. Edinburgh University, 1988.
[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.
[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.
[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.

Reference Title: References

Reference Type: bibliography

[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.
[2] P. Audebaud and C. Paulin-Mohring . Proofs of randomized algorithms in Coq. To appear in Science of Computer Programming. Extended version of [1].
[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.
[4] Y. Bertot and P. Castéran . Interactive Theorem Proving and Program Development. Springer-Verlag, 2004.
[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.
[6] V. Capretta . General recursion via coinductive types. Logical Methods in Computer Science, 1(2:1):1–28, 2005.
[7] P. Caspi and M. Pouzet . Synchronous Kahn Networks. In ACM SIGPLAN International Conference on Functional Programming, Philadelphia, Pensylvania, May 1996.
[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.
[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.
[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.
[11] G. Kahn . The semantics of a simple language for parallel programming. In Information Processing 74. North-Holland, 1974.
[12] G. Kahn and D. MacQueen . Coroutines and networks of parallel processes. In B. Gilchrist (ed.) Information Processing 77. North-Holland, 1977.
[13] G. Kahn and G. D. Plotkin . Concrete domains. Theoretical Computer Science, 121(1& 2):187–277, 1993.
[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.
The Coq Development Team . The Coq Proof Assistant Reference Manual – Version V8.1, July 2006. http://coq.inria.fr.

Reference Title: References

Reference Type: bibliography

[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.
[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.
[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.
[4] N. Ayache (ed.) Computational Models for the Human Body. Handbook of Numerical Analysis (Ph. Ciarlet series editor). Elsevier, 2004. 670 pages.
[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.
[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.
[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.
[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.
[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.
[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.
[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.
[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.
[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.
[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.
[15] I. L. Dryden and K. V. Mardia . Statistical Shape Analysis. John Wiley and Sons, 1998.
[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.
[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.
[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.
[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.
[20] N. C. Fox and J. M. Schott . Imaging cerebral atrophy: normal ageing to Alzheimer's disease. Lancet, 363(9406), 2004.
[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.
[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.
[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.
[24] P. Hunter . Computational physiology and the physiome project, 2004. “http://nbcr.sdsc.edu/mcmregistration/pdf/Peter_Hunter.pdf”.
[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.
[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.
[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.
[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.
[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.
[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] 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.
[32] G. Picinbono , H. Delingette and N. Ayache . Non-linear anisotropic elasticity for real-time surgery simulation. Graphical Models, 65(5):305–321, 2003.
[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.
[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.
[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. 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.
[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.
[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.
[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.
[40] D. W. Thompson . On Growth and Form. Cambridge University Press, 1917.
[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] 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] 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] 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.

Reference Title: References

Reference Type: bibliography

[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.
[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.
[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.
[4] F. Baccelli and P. Bremaud . Elements of Queueing Theory, 2nd ed. Wiley, 2003.
[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.
[6] F. Baccelli , G. Carofiglio and S. Foss . Proxy Caching in split TCP: Dynamics, Stability and Tail Asymptotics, INRIA Report, July 2007.
[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.
[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.
[9] A. Bakre and B. R. Badrinath . I-TCP: Indirect TCP for Mobile Hosts. Proceedings of the 15th ICDCS, May 1995.
[10] A. V. Bakre and B. R. Badrinath , Implementation and performance evaluation of Indirect TCP. IEEE Transactions on Computers, 46(3):260–278, 1997.
[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.
[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.
[13] P. Embrechts , C. Kluppelberg and T. Mikosch Modelling Extremal Events. Springer, 1997.
[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.
[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.
[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.
[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.
[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.
[19] G. Kwon and J. Byers . ROMA: reliable overlay multicast with loosely coupled TCP connections. Proceedings of the IEEE Infocom, February 2004.
[20] M. Luglio , M. Y. Sanadidi , M. Gerla and J. Stepanek . On-board satellite “split TCP” proxy. IEEE JSAC, 22(2), 2004.
[21] T. Liggett , An improved subadditive ergodic theorem. Annals of Probability, 13:1279–1285, 1985.
[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] I. Norros , A storage model with self-similar input, Queueing Systems, 16:387–396, 1994.
[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.
[25]http://www.ietf.org/rfc/rfc3135.txt.
[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.
[27] A. Sundararaj and D. Duchamp . Analytical characterization of the throughput of a split TCP connection. Technical Report, Stevens Institute of Technology, 2003.
[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.
[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.

Reference Title: References

Reference Type: bibliography

[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.
[2] T. H. Clutton-Brock . The Evolution of Parental Care, University Press, Oxford, 1991.
[3] M. Doebeli and C. Hauert . Models of cooperation based on Prisoner's dilemma and Snowdrift games. In Ecology Letters, 8:748–756, 2005.
[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.
[5] R. A. Fisher . The Genetical Theory of Natural Selection, University Press, Oxford, 1930.
[6] F. Hamelin . Jeux dynamiques en écologie du comportement. thèse de doctorat, Université de Nice, soutenue le 4 juillet 2007.
[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.
[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.
[9] A. I. Houston , T. Szekely and J. M. McNamara . Conflict between parents over care. Trends in Ecology and Evolution, 20:33–38, 2005.
[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.
[11] J. M. McNamara , et al. A dynamic game-theoretic model of parental care. Journal of Theoretical Biology 205:605–623, 2000.
[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)
[13] L. Samuelson . Evolutionary Games and Equilibrium Selection. MIT Press, 1998.
[14] W. H. Sandholm . Population Games and Evolutionary Dynamics. Preprint, http://www.ssc.edu/∼whs/book/index.html, 2007.
[15] J. G. Wardrop . Some theoretical aspects of road trafic. Proceedings of the Institution of Civil Engineers, Part II, 1:325–378, 1952.
[16] T. Winquist and R. E. Lemon . Sexual selection and exaggerated male tail length in birds. The American Naturalist, 143:95–116, 1994.
[17] A. Zahavi . Mate selection – a selection for the handicap. Journal of Theoretical Biology, 53:205–214, 1975.

Reference Title: References

Reference Type: bibliography

[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.
[2] A. Carle and M. Fagan . ADIFOR 3.0 overview. Technical Report CAAMTR-00-02, Rice University, 2000.
[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.
[4] C. Faure and U. Naumann . Minimizing the tape size. In [3], chapter VIII, pp. 293–298. 2002.
[5] C. Faure and Y. Papegay . Odyssée User's Guide. Version 1.7. Technical report 224, INRIA, 1998.
[6] R. Giering . Tangent linear and Adjoint Model Compiler, Users manual. Technical report, 1997. http://www.autodiff.com/tamc.
[7] R. Giering and T. Kaminski . Generating recomputations in reverse mode AD. In [3], chapter VIII, pp. 283–291. 2002.
[8] A. Griewank . Evaluating Derivatives: Principles and Techniques of Algorithmic Differentiation. SIAM, Frontiers in Applied Mathematics, 2000.
[9] L. Hascoët . The Data-dependence Graph of Adjoint Programs. Research Report 4167, INRIA, 2001.
[10] L. Hascoët and M. Araya-Polo . The adjoint data-flow analyses: Formalization, properties, and applications. In [1], pp. 135–146. 2006.
[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.
[12] L. Hascoët and V Pascual . Tapenade 2.1 user's guide. Technical report 300, INRIA, 2004.
[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] U. Naumann . Optimal Jacobian accumulation is NP-complete. Mathematical Programing, 2006. in press. Appeared online first.
[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] J. Nocedal and S.-J. Wright . Numerical Optimization. Springer, Series in Operations Research, 1999.
[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.
[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.

Reference Title: References

Reference Type: bibliography

[1] Debugging advice can be found at http://www.wikihow.com/Debug-a-Tamagotchi.
[2] Y. Lazebnik . Can a biologist fix a radio? Or, what I learned while studying apoptosis. Cancer Cell 2:179–182, 2002.
[3] E. Klipp , R. Herwig , A. Kowald , C. Wierling and H. Lehrach . Systems Biology in Practice. Wiley, 2005.
[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.
[5] Bandai . Tamagotchi Connection. http://www.tamagotchi.com
[6] P. Tonella and A. Potrich . Reverse Engineering of Object-Oriented Code. Springer, 2005.
[7] S. Brenner . Interview. Discover Magazine 25(4), 2004.
[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.
[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.

Reference Title: References

Reference Type: bibliography

[1] S. Emmott (ed.). Towards 2020 Science, available from http://www.research.microsoft.com/towards2020science.
[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.
[3] C. Ferris and J. Farrell . What are web services? CACM 46(6):31, 2003.
[4] M. Lesk . Online Data and Scientific Progress: Content in Cyberin-frastructure. http://archiv.twoday.net/stories/337419/, 2004 [Accessed 6 December 2005].
[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.
[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.
[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.
[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.
[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.
[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.
[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.
[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.

Reference Title: References

Reference Type: bibliography

[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.
[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.
[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.
[4] Aho, Sethi, Ullman . Compiler Writing: Principles Programming and Tools, Addison Wesley, 1986.
[5] Y. Coscoy , G. Kahn and L. Théry . Extracting text from proofs. In Typed Lambda Calculi and Applications TLCA'95, Edinburgh.
[6] Y. Coscoy . A natural language explanation for formal proofs. In Logical Aspects of Computational Linguistics, LACL'96, Nancy France.
[7] L. Théry , Y. Bertot and G. Kahn . Real theorem provers deserve real user-interfaces. ACM SIGSOFT Symposium on Software Development Environments. 1992.
[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.
[9]The Calculus of Constructions. Documentation and User's Guide, Version 4.10. Technical Report 110, INRIA, 1989.
[10] C. Paulin-Mohring and B. Werner . Synthesis of ML programs in the system Coq. Journal of Symbolic Computation 15:607–640, 1993.