• Isar

  • Referenced in 145 articles [sw04599]
  • alternative proof language interface layer, beyond traditional tactic scripts. The Isabelle/Isar system provides an interpreter...
  • ArcAngel

  • Referenced in 14 articles [sw01812]
  • ArcAngel: a tactic language for refinement. Morgan’s refinement calculus is a successful technique ... commonly used development strategies, documenting them as tactics, and using them as single transformation rules ... language for defining such refinement tactics; we present the language, its semantics, and some ... Apart from Angel, a general-purpose tactic language that we are extending, no other tactic...
  • mural

  • Referenced in 9 articles [sw23627]
  • with VDM. Chapter 5 presents the tactic language which allows the user to compose sequences...
  • ArcAngelC

  • Referenced in 6 articles [sw06338]
  • ArcAngelC: a Refinement Tactic Language for Circus. Circus is a refinement language in which specifications ... used, and by documenting them as tactics, they can be expressed and repeatedly applied ... Here, we present ArcAngelC, a language for defining such tactics; we present the language...
  • Isabelle/UTP

  • Referenced in 14 articles [sw21184]
  • proof obligations in the object-language. Thirdly, proof tactics that transfer results from well-supported ... insights towards reconciliation of shallow and deep language embeddings...
  • Mtac

  • Referenced in 14 articles [sw13075]
  • Mtac: a monad for typed tactic programming in Coq. Effective support for custom proof automation ... interactive proof development. However, existing languages for automation via tactics either (a) provide...
  • Rtac

  • Referenced in 3 articles [sw13124]
  • Rtac – a reflective tactic language for Coq. Computational reflection is a useful technique for avoiding ... tactics. Can we build a lightweight tactic language for building reflective procedures easily? To this ... Rtac, a lightweight, work-in-progress, tactic language built on top of MirrorCore, a parametric...
  • Bellerophon

  • Referenced in 4 articles [sw23943]
  • those insights. We present a tactics language and library for hybrid systems verification, named Bellerophon ... prover. Among the automation that emerges are tactics for decomposing hybrid systems, discovering and establishing ... syntax and semantics for the Bellerophon tactic combinator language, culminating in an example verification effort...
  • Matita

  • Referenced in 72 articles [sw06140]
  • machine collaboration. It provides a formal language where mathematical definitions, executable algorithms and theorems cohexist ... updating it according to commands (usually called tactics) issued by the user...
  • VeriML

  • Referenced in 8 articles [sw13522]
  • lack of a single language where users can develop complex tactics and decision procedures using ... specific tactics and decision procedures.par In this paper, we present VeriML -- a novel language design ... require significant additions to the logic language, so soundness is guaranteed. We have built ... showing a number of type-safe tactics and decision procedures written in VeriML...
  • KeYmaera X

  • Referenced in 13 articles [sw40558]
  • layer of tactics on top of the prover kernel provides a rich language for implementing...
  • Mollusc

  • Referenced in 2 articles [sw32624]
  • automated proof construction through a tactic language and interpreter...
  • EXPANDER

  • Referenced in 6 articles [sw22715]
  • plans, strategies or tactics. It is written in the functional language SML/NJ. EXPANDER executes single...
  • Irdis

  • Referenced in 22 articles [sw09690]
  • general purpose pure functional programming language with dependent types. Dependent types allow types ... idiom brackets; Indentation significant syntax; Extensible syntax; Tactic based theorem proving (influenced by Coq); Cumulative...
  • Fiat

  • Referenced in 14 articles [sw21357]
  • written using libraries of specification languages for describing common programming tasks like querying a relational ... iteratively refined into efficient implementations via automated tactics. Each derivation in Fiat produces a formal...
  • Eisbach

  • Referenced in 8 articles [sw13077]
  • accessible to existing users. We describe the language and the design principles on which ... evaluate its effectiveness by implementing some tactics widely-used in the seL4 verification stack...
  • MMode

  • Referenced in 3 articles [sw24341]
  • Abstract. We present a set of tactics for version 7.4 of the Coq proof assistant ... write proofs for Coq in a language ... similar to the proof language of the Mizar system. These tactics can be used with...
  • miz3

  • Referenced in 11 articles [sw18631]
  • uses is a slight variant of the language of the Mizar system ... easy access to the full set of tactics and formal libraries of HOL Light ... declarative systems have essentially the same proof language, this give s a straightforward...
  • Charge!

  • Referenced in 10 articles [sw22731]
  • separation-logic proof outlines. In particular, the tactics allow the user to reason ... also independent of the choice of programming language...
  • KeYmaeraD

  • Referenced in 0 articles [sw20142]
  • have designed a powerful strategy and tactics language for directing proof search. With these techniques...