• LEGO

  • Referenced in 107 articles [sw09685]
  • more practical by bringing the level of formalization closer to that of informal mathematics ... theories, and the support of specifying new inductive types, provide an expressive language for formalization...
  • Grail

  • Referenced in 19 articles [sw00374]
  • state machines, regular expressions, and other formal language theory objects. Using Grail, one can input...
  • GOLOG

  • Referenced in 170 articles [sw02159]
  • abstraction than is usually possible. The language appears well suited for applications in high level ... based on a formal theory of action specified in an extended version of the situation...
  • Isabelle/ZF

  • Referenced in 62 articles [sw04973]
  • computer languages and protocols. Isabelle/ZF formalizes the greater part of elementary set theory, including relations...
  • ForTheL

  • Referenced in 8 articles [sw09797]
  • formal theories. ForTheL, an acronym for “Formal Theory Language”, is a formal language of mathematical...
  • Myhill-Nerode

  • Referenced in 10 articles [sw28547]
  • paper that a central result from formal language theory -- the Myhill-Nerode Theorem...
  • FAdo

  • Referenced in 14 articles [sw10335]
  • tools for symbolic manipulation of formal languages. To allow high-level programming with complex data ... pedagogical tool for teaching automata theory and formal languages. For the graphical visualization and interactive...
  • PiDuce

  • Referenced in 21 articles [sw01418]
  • technologies The PiDuce project comprises a programming language and a distributed runtime environment devised ... relying on solid theories about process calculi and formal languages for XML documents and schemas.The...
  • GUItar

  • Referenced in 10 articles [sw10336]
  • tools for symbolic manipulation of formal languages. To allow high-level programming with complex data ... pedagogical tool for teaching automata theory and formal languages. For the graphical visualization and interactive...
  • CP-logic

  • Referenced in 17 articles [sw06947]
  • representation for his semantical objects. Second, this language also has relevance for the area ... prove that the formal semantics of a theory in our language can be equivalently defined ... models of certain logic programs, rendering it formally quite similar to existing languages such...
  • Z

  • Referenced in 278 articles [sw10291]
  • specification language $Z$. It is primarily directed to the user; the background theory is -- with ... this adquate for promoting a discipline of formal specification and reasoning? Another disappointment is that...
  • Cyto-Sim

  • Referenced in 5 articles [sw35368]
  • underlying model is based on formal language theory and has been shown to have decidable ... properties (Cavaliere and Sedwards, 2006), allowing formal analysis in addition to simulation. The simulator provides...
  • Why3

  • Referenced in 128 articles [sw04438]
  • comes with a standard library of logical theories (integer and real arithmetic, Boolean operations, sets ... WhyML is also used as an intermediate language for the verification of C, Java ... features are: numerous extensions to the input language, a new architecture for calling external provers ... user a possibility to easily reuse Why3 formalizations or to add support...
  • Isar

  • Referenced in 140 articles [sw04599]
  • interpreter for the Isar formal proof document language. Isabelle/Isar input consists either of proper document ... integrated into the Isabelle/Pure meta-logic implementation. Theories, theorems, proof procedures etc. may be used...
  • XDuce

  • Referenced in 54 articles [sw12436]
  • language. XDuce is a statically typed programming language for XML processing. Its basic data values ... theory of regular tree automata, and present a complete formal definition of its core, along...
  • MMT

  • Referenced in 47 articles [sw07136]
  • language, which provides a simple and scalable Module system for the development of Mathematical Theories ... meta-logical level. This ”logics-as-theories” approach makes system behaviors as well as their ... modular mathematical theories. Thus, it provides an interface layer between formally rigorous mathematical systems...
  • Mathematical Components

  • Referenced in 3 articles [sw30935]
  • extensive and coherent repository of formalized mathematical theories. It is based on the Coq proof ... assistant, powered with the Coq/SSReflect language. These formal theories cover a wide spectrum of topics...
  • LPL software

  • Referenced in 18 articles [sw04860]
  • Language, Proof and Logic covers topics such as the boolean connectives, formal proof techniques, quantifiers ... basic set theory, and induction. Advanced chapters include proofs of soundness and completeness for propositional...
  • JavaFAN

  • Referenced in 30 articles [sw01934]
  • explicit state model checking. Both Java language and JVM bytecode analyses are possible. JavaFAN ... lines of Maude code, specifying formally the semantics of Java and JVM in rewriting logic ... search and LTL model checking of rewriting theories...
  • ArchJava

  • Referenced in 19 articles [sw01803]
  • enabling more effective design, program understanding, and formal analysis. However, existing approaches decouple implementation code ... publications describing the language, a case study, and the theory behind ArchJava...