• # Z

• Referenced in 286 articles [sw10291]
• Using Z. Specification, refinement, and proof. The book is an in-depth introduction ... with the exception of the natural deduction calculus, see below -- only introduction ... integration of $Z$ with the refinement calculus and data refinement. The overall presentation is fluent ... tedious exposition of the natural deduction calculus, which is not used further...
• # ZRC

• Referenced in 14 articles [sw21827]
• Refinement Calculus for Z. The fact that Z is a specification language only, with ... that, we present ZRC, a refinement calculus based on Morgan’s work that incorporates ... conventions. This work builds upon existing refinement techniques for Z, but distinguishes itself mainly ... laws of ZRC. More than a refinement calculus, ZRC is a theory of refinement...
• # ArcAngel

• Referenced in 14 articles [sw01812]
• tactic language for refinement. Morgan’s refinement calculus is a successful technique for developing software ... present ArcAngel, a language for defining such refinement tactics; we present the language, its semantics...
• # Isabelle/Circus

• Referenced in 13 articles [sw15208]
• with a refinement calculus. Its semantics is based on Hoare and He’s unifying theories ... support that finally allows for proofs of refinement for Circus processes (involving both data...
• # LEGO

• Referenced in 108 articles [sw09685]
• Calculus of Constructions (CC), the Generalized Calculus of Constructions (GCC) and the Unified Theory ... natural deduction style. It supports refinement proof as a basic operation. The system design emphasizes...
• # F*

• Referenced in 20 articles [sw27563]
• dependent types, monadic effects, refinement types, and a weakest precondition calculus. Together, these features allow...
• # FAUST2

• Referenced in 14 articles [sw23682]
• computations and fast manipulations based on vector calculus. The abstract model is formally ... reach-avoid) over the abstract model, and refine the outcomes over the concrete dtMP...
• # JavaSPI

• Referenced in 3 articles [sw23647]
• language that corresponds to applied $pi$-calculus. This Java model can be symbolically executed ... debugger, formally verified with ProVerif, and further refined to an interoperable Java implementation...
• # Alpha

• Referenced in 6 articles [sw13717]
• uniformization, parallelization for instance), the description is refined until it may be interpreted ... parallelization, code generation, language semantics, convex polyhedra calculus, abstract and non-standard interpretation, program verification...
• # TimeSquare

• Referenced in 4 articles [sw15830]
• functional, elastic (can be abstracted or refined) and multiform. TimeSquare is based on the latest ... based editor of constraints, a polychronous clock calculus engine able to process a partial order...
• # mkbTT

• Referenced in 6 articles [sw10018]
• tools. Knuth-Bendix completion is a classical calculus in automated deduction for transforming ... pair criteria and isomorphisms are presented as refinements together with all proofs. We furthermore describe...