Abstract
Rigorous program development is notoriously difficult because it involves many aspects, among which specification, programming, verification, code reuse, maintenance, and version management. Besides, these various tasks are interdependent, requiring going back and forth between them. In this paper, we are interested in certain language features and in languages which help make the user’s life easier for developing programs satisfying their specifications.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
The Agda proof assistant, http://www.cs.chalmers.se/~catarina/agda/
Borovanský, P., Kirchner, C., Kirchner, H., Moreau, P.-E., Vittek, M.: ELAN: A logical framework based on computational systems. In: Meseguer, J. (ed.) 1st International Workshop on Rewriting Logic and its Applications. Electronic Notes in Theoretical Computer Science, vol. 4 (1996)
Bouhoula, A., Jouannaud, J.-P., Meseguer, J.: Specification and proof in membership equational logic. Theoretical Computer Science 236, 35–132 (1999)
Bracha, G.: The Programming Language Jigsaw: Mixins, Modularity and Multiple Inheritance. PhD thesis, Dept. of Computer Science, University of Utah (1992)
Brodal, G.S., Okasaki, C.: Optimal purely functional priority queues. Journal of Functional Programming 6(6), 839–857 (1996)
Burstall, R.M., Goguen, J.A.: Burstall and Joseph A. Goguen. Putting theories together to make specifications. In: Proc. 5th International Joint Conference of Artificial Intelligence, Cambridge Massachusetts, pp. 1045–1058. Edinburgh University, Edinburgh (1977)
Burstall, R.M., Goguen, J.A.: The semantics of CLEAR, a specification language. In: Abstract Software Specifications. LNCS, vol. 86, Springer, Heidelberg (1980)
Chrząszcz, J.: Modules in Coq are and will be correct. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol. 3085, pp. 130–146. Springer, Heidelberg (2004)
Clavel, M., Eker, S., Lincoln, P., Meseguer, J.: Principles of Maude. In: Meseguer, J. (ed.) 1st International Workshop on Rewriting Logic and its Applications. Electronic Notes in Theoretical Computer Science, vol. 4 (1996)
The Coq proof assistant, http://coq.inria.fr/
Coquand, T., Huet, G.: The calculus of constructions. Information and Computation 76, 95–120 (1988)
Thierry Coquand and Christine Paulin-Mohring. Inductively defined types. In P. Martin-Löf and G. Mints, editors, COLOG-88: International conference on computer logic, volume 417 of LNCS. Springer-Verlag, 1990.
Filliâtre, J.-C., Letouzey, P.: Functors for Proofs and Programs. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 370–384. Springer, Heidelberg (2004)
Futatsugi, K., Goguen, J.A., Jouannaud, J.-P., Meseguer, J.: Principles of OBJ2. In: Proc. 12th ACM Symp. on Principles of Programming Languages, New Orleans (1985)
Goguen, J.A., Thatcher, J.W., Wagner, E.G.: An initial algebra approach to the specification, correctness and implementation of abstract data types. In: Current Trends in Programming Methodology, vol. 4, pp. 80–149. Prentice Hall, Englewood Cliffs (1978)
Goguen, J.A., Thatcher, J.W., Wagner, E.W., Wright, J.B.: Initial algebra semantics and continuous algebra. Journal of the ACM 24(1), 68–95 (1977)
Goguen, J.A., Tardo, J.J.: An introduction to obj, a language for writing and testing formal algebraic specifications. In: Specification of Reliable Software Conference, April 1979, pp. 170–189 (1979)
Goguen, J.A., Winkler, T., Meseguer, J., Futatsugi, K., Jouannaud, J.-P.: Introducing OBJ*. In: Coleman, D., Gallimore, R., Goguen, J.A. (eds.) Applications of Algebraic Specifications Using OBJ, Cambridge University Press, Cambridge (1993)
Hirschowitz, T., Leroy, X.: Mixin modules in a call-by-value setting. In: Le Métayer, D. (ed.) ESOP 2002. LNCS, vol. 2305, pp. 6–20. Springer, Heidelberg (2002)
Kirchner, C., Kirchner, H., Meseguer, J.: Operational semantics of OBJ3. In: Lepistö, T., Salomaa, A. (eds.) ICALP 1988. LNCS, vol. 317, pp. 287–301. Springer, Heidelberg (1988)
The LEGO proof assistant, http://www.dcs.ed.ac.uk/home/lego/
Luo, Z.: ECC an Extended Calculus of Constructions. In: 4th Symposium on Logic in Computer Science, Pacific Grove, California (1989)
MacQueen, D.: Theory and practice of higher-order type systems or the Standard ML type system. Copy of Transparencies
Magnusson, L., Nordström, B.: The alf proof editor and its proof engine. In: Barendregt, H., Nipkow, T. (eds.) TYPES 1993. LNCS, vol. 806, pp. 213–237. Springer, Heidelberg (1994)
Martin-Löf, P.: An intuitionistic theory of types: Predicative part. In: Rose, H.E., Sheperdson, J.C. (eds.) Logic Colloquium 1973 Studies in Logic, vol. 80, pp. 73–118. North-Holland, Amsterdam (1975)
Martin-Löf, P.: Intuitionistic Type Theory, Biblioplois, Napoli. Notes of Giowanni Sambin on a series of lectues given in Padova (1984)
Milner, R.: A theory of type polymorphism programming. Journal of Computer and System Sciences 17 (1978)
Nakajima, S., Futatsugi, K.: An object-oriented modeling method for algebraic specifications in Cafe OBJ. In: 19th International Conference on Software Engineering, pp. 34–44. ACM Press, New York (1997)
The Objective Caml language, http://caml.inria.fr/
Weis, P., et al.: The CAML reference manual. Rapport de Recherche 121, INRIA (1990)
Werner, B.: Méta-théorie du Calcul des Constructions Inductives. PhD thesis, Univ. Paris VII (1994)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Chrząszcz, J., Jouannaud, JP. (2006). From OBJ to ML to Coq. In: Futatsugi, K., Jouannaud, JP., Meseguer, J. (eds) Algebra, Meaning, and Computation. Lecture Notes in Computer Science, vol 4060. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11780274_12
Download citation
DOI: https://doi.org/10.1007/11780274_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-35462-8
Online ISBN: 978-3-540-35464-2
eBook Packages: Computer ScienceComputer Science (R0)