Theorema is a project that aims at supporting the entire process of mathematical theory
exploration within one coherent logic and software system. This survey paper illustrates the …

In this paper, we address the question of how to automatically map computational kernels to
highly efficient code for a wide range of computing platforms and establish the correctness of …

Data locality and parallelism are critical optimization objectives for performance on modern
multi-core machines. Both coarse-grain parallelism (eg, multi-core) and fine-grain …

This roadmap describes ways that researchers in four areas---specification languages,
program generation, correctness by construction, and programming languages---might help …

Abstract We present the Operator Language (OL), a framework to automatically generate
fast numerical kernels. OL provides the structure to extend the program generation system …

This paper presents a mechanizable framework for specifying, developing, and reasoning
about complex systems. The framework combines features from algebraic specifications …

Recently, we proposed a systematic method for top-down synthesis and verification of
lemmata and algorithms called “lazy thinking method” as a part of systematic mathematical …

Over the last two years, we have demonstrated the feasibility of applying category-theoretic
methods in specifying, synthesizing, and maintaining industrial strength software systems …

This paper presents an overview of the technical foundations and current directions of
Kestrel's approach to mechanizing software development. The approach emphasizes …

We advocate an automated refinement approach to developing programs and their proofs.
The approach is partially embodied in the Specware system [6] which has found industrial …