Baby Modula-3
Baby Modula-3 is a functional programming sublanguage of Modula-3 (safe subset) programming language based on ideals invented by Martín Abadi. It is an object-oriented programming language for studying programming language design; one part of it is implicitly prototype-oriented, and the other is explicitly statically typed designed for studying computer science type theory. It has been checked as a formal language of metaprogramming systems.[1] It comes from the Scandinavian School of object-oriented languages.
Abadi tried to give an example of pure object-oriented language which would allow studying the formal semantics of objects. "Baby Modula-3 is defined with a structured operational semantics and with a set of static type rules. A denotational semantics guarantees the soundness of this definition."[1] This object model has been shown to have well definiteness decidability[2] (a mechanical proof of it isn't known).
Abadi worked at Digital Equipment Corporation (DEC) Systems Research Center (SRC) in Palo Alto, California . As DEC was bought by Compaq and then Compaq was bought by Hewlett-Packard (HP), the SRC-report 95 was made available to the public by HP.
Influences
Luca Cardelli and Martín Abadi wrote the book A Theory of Objects in 1996,[3] laying out formal calculi for the semantics of object-oriented programming languages. Baby Modula-3 influenced this work according to Cardelli,[4] and guided a calculus of the type of self in Types for object and the type of 'self'.[5] It has opened the way for work on Modula-3 formal semantic checking systems, for object-oriented type system programming languages that have been used to model the formal semantics of languages such as Ada and C.[6]
References
- ↑ 1.0 1.1 Baby Modula-3 and a theory of objects Martin Abadi. Digital Equipment Corporation (DEC) Systems Research Center (SRC) Research Report 95 (February 1993)
- ↑ Schwinghammer, J. (2008-01-01). "On Normalization by Evaluation for Object Calculi". in Miculan, Marino; Scagnetto, Ivan; Honsell, Furio. Types for Proofs and Programs. Lecture Notes in Computer Science. 4941. Springer Berlin Heidelberg. pp. 173–187. doi:10.1007/978-3-540-68103-8_12. ISBN 978-3-540-68084-0.
- ↑ A Theory of Objects (Corrected ed.). Springer. 1996-08-09. ISBN 978-0387947754.
- ↑ A Theory of Primitive Objects (untyped, first and second-order systems), http://reference.kfupm.edu.sa/content/t/h/a_theory_of_primitive_objects__661478.pdf, retrieved 2012-03-29
- ↑ Abstracts of papers presented to the American Mathematical Society. American Mathematical Society. 1995.
- ↑ Research, http://people.cis.ksu.edu/~bhoward/res.ps, retrieved 2012-03-22
 |  |
