Re: applications of TYPOL

[jmi@columbo.inria.fr (Janet Bertot)]

In article <DSTJun7.145945.5463@sophia.inria.fr>, mpe@ida.liu.se (Mikael Pettersson) writes:
> Is there an up-to-date list of languages that have TYPOL
> specifications of their semantics? (Preferably with some
> indication on where one can get these specifications.)

An up-to-date list, does not exist.  i've a list of languages which 
had either the syntax and/or semantics under Centaur but even this 
list was constructed based on people who responded to a call for 
abstracts of what our users do with Centaur, or people who actually
attended a users group meeting last year in Sophia.

Depending on the language people have done interpreters, simulators,
typecheckers, various translators etc.   Of course, the specifications
for these are either written in Typol or ASF.  The only example that 
i can think of offhand that meets your second requirement

	> A colleague of mine is particularly interested in the Natural
	> Semantics of realistic OO languages.

would be EIFFEL.  Both the static and dynamic semantics have been
specified, if memory serves the static semantics exists in ASF, while
while the dynamic semantics is in Typol.  

For completeness, the list compiled at the last centaur users group meeting:

Languages specified using Centaur:
-------------------------------------

Below is a list of languages that have been specified with
one or more of the Centaur formalisms (Metal, SDF, Typol, ASF).
Of course, all the Centaur formalisms mentioned above and,
additionally, PPML also have associated Centaur environments.

C, Ada, Pascal, Fortran77/90, Le Lisp, 
Esterel, Lustre, VDM, LOTOS, ASN1*, EIFFEL*,
VHDL, ADL, ALPHA, SIGNAL, MANIFOLD, mu-CRL, L, SETL

NB: (*) subsets of the language have been described under Centaur.



A more detailed breakdown:
--------------------------

C, Pascal, Ada (syntax only)

Fortran77/90 (syntax only for Connexite S.A.'s Fortran77/90 environment)
	     (a number of transformations written in either Typol, C, 
	      or LeLisp for parallelizations/vectorization.)

Le Lisp (syntax only, the interpreter comes for free :-)

Esterel (syntax + interpreter in Typol)

Lustre (syntax + interpreter in Typol)
 
VDM (syntax + static semantics, translator VDM to ADA)

LOTOS (syntax + typechecker, simulator)

ASN1 (syntax, typechecker, optimizer, test generator)

EIFFEL (syntax, static and dynamic semantics)

VHDL (syntax for VHDL87)

ADL, a first order functional language (syntax, typechecker, interpreter)

ALPHA, an equational language to specify dataflow (e.g., systolic arrays)
	(syntax + translators to generate VHDL or Model code)

SIGNAL, language for signal programming (syntax)

MANIFOLD, a parallel programming language (syntax + semantics)

mu-CRL, process description language (syntax, typechecker, simulator)

L, a data parallel language (syntax, simulator, generator of verification
	conditions)

SETL (syntax in Metal + translation to ADA using Typol)

	
		--janet