Mathematical software

Crowfoot
Referenced in 5 articles [sw07706]
Crowfoot: A verifier for higher-order store programs. We present Crowfoot, an automatic verification tool ... these programs use a heap that can store not only data but also code (commands ... procedures). Such heaps are often called higher-order store, and allow for instance the creation ... higher-order store to model phenomena such as runtime loading and unloading of code, runtime...

Ynot
Referenced in 35 articles [sw12334]
supports writing, reasoning about, and extracting higher-order, dependently-typed programs with side-effects ... such as non-termination, accessing a mutable store, and throwing/catching exceptions.The axioms of Ynot form ... abstraction mechanisms of Coq to build higher-level reasoning mechanisms which in turn ... finite maps, including support for a higher-order (effectful) iterator. The implementations range from simple...

Diamanlab
Referenced in 2 articles [sw26170]
stored in checkpoints. Theoretical aspects and implementation are generic, taking advantage of the efficient higher ... order asymptotic numerical method in its Diamant form that interprets the generic nonlinear problem...

Watson
Referenced in 1 article [sw25432]
equational higher-order theorem prover. The higher-order logic supported by the prover is distinctive ... automated proof strategies, which are represented and stored by the prover in the same...

Crowfoot