
Coq
 Referenced in 1856 articles
[sw00161]
 proofs. Typical applications include the formalization of programming languages semantics (e.g. the CompCert compiler certification ... Card EAL7 certification in industrial context), the formalization of mathematics (e.g. the full formalization...

ML
 Referenced in 517 articles
[sw01218]
 completely specified and verified using formal semantics. Its types and pattern matching make it well ... commonly used to operate on other formal languages, such as in compiler writing, automated theorem...

SPARQL
 Referenced in 132 articles
[sw07429]
 SPARQL standard presenting its syntax and formal semantics. We then focus on the formalization ... important recently discovered issues regarding the normative semantics of federation and navigation in SPARQL...

Ptolemy
 Referenced in 78 articles
[sw07459]
 modular formal semantics for Ptolemy. Ptolemy is an opensource and extensible modelling and simulation ... arbitrary fashion. This paper proposes a formal semantics for Ptolemy that is modular ... models of computation. In this paper, we formally define the directors for the following models...

PDDL
 Referenced in 96 articles
[sw07079]
 syntax of the language, its formal semantics and the validation of concurrent plans. We observe...

KLAIM
 Referenced in 71 articles
[sw09424]
 interaction protocols among located processes. The formal operational semantics is useful for discussing the design...

WSAT
 Referenced in 37 articles
[sw01022]
 service standards, most of which lack formal semantics, complicate the formal specification of web service...

PNML
 Referenced in 40 articles
[sw03257]
 Petri nets, ISO/IEC 15909, provides a formal semantics and syntax to enable model interchange...

Isar
 Referenced in 144 articles
[sw04599]
 approach to readable formal proof documents sets out to bridge the semantic gap between internal ... abstraction for userlevel work. The Isar formal proof language has been designed to satisfy...

MANIFOLD
 Referenced in 30 articles
[sw02900]
 transition system semantics for the controldriven coordination language MANIFOLD Coordination languages ... supported by MANIFOLD. We present the formal semantics of a kernel of MANIFOLD, based ... semantics of a controloriented coordination language, this approach is useful for the formal studies...

RuleML
 Referenced in 27 articles
[sw01792]
 language for rules using XML markup, formal semantics, and efficient implementations.RuleML covers the entire rule...

GROOVE
 Referenced in 50 articles
[sw09480]
 model transformation and operational semantics. This entails a formal foundation for model transformation and dynamic...

qGCL
 Referenced in 26 articles
[sw39240]
 including initialisation and observation), has a formal semantics and body of laws, and provides...

Ruby
 Referenced in 33 articles
[sw16267]
 meet this challenge, we present a formal operational semantics that can serve as a high...

HOLOCL
 Referenced in 21 articles
[sw05734]
 issues of the design of a formal semantics of the OCL. Thecs...

JavaFAN
 Referenced in 32 articles
[sw01934]
 lines of Maude code, specifying formally the semantics of Java and JVM in rewriting logic...

COMAL
 Referenced in 55 articles
[sw30775]
 computers. The ”COMAL Kernel Syntax & Semantics”[1] contains the formal definition of the language. Further...

CPlogic
 Referenced in 17 articles
[sw06947]
 aspect, which has been studied at the semantical level by Shafer in his framework ... this evolution is quite natural. In our formalization, a set of probabilistic causal laws ... offering a convenient logical representation for his semantical objects. Second, this language also has relevance ... particular, we prove that the formal semantics of a theory in our language...

Metropolis
 Referenced in 17 articles
[sw16265]
 challenge. Based on a metamodel with formal semantics that developers can use to capture designs ... complex electronicsystem design that supports simulation, formal analysis, and synthesis...

Isabelle/Circus
 Referenced in 13 articles
[sw15208]
 with a refinement calculus. Its semantics is based on Hoare and He’s unifying theories ... develop a machinechecked, formal semantics based on a “shallow embedding” of Circus in Isabelle/UTP...