Sökning: "SSReflect"

Hittade 2 avhandlingar innehållade ordet SSReflect.

  1. 1. Formalizing Refinements and Constructive Algebra in Type Theory

    Författare :Anders Mörtberg; Göteborgs universitet; Göteborgs universitet; Gothenburg University; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Formalization of mathematics; refinements; constructive algebra; type theory; Coq; SSReflect;

    Sammanfattning : The extensive use of computers in mathematics and engineering has led to an increased demand for reliability in the implementation of algorithms in computer algebra systems. One way to increase the reliability is to formally verify that the implementations satisfy the mathematical theorems stating their specification. LÄS MER

  2. 2. Constructive Algebra in Type Theory

    Författare :Anders Mörtberg; Göteborgs universitet; Göteborgs universitet; Gothenburg University; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES;

    Sammanfattning : This thesis contains four papers aiming at bridging the gap between algorithms implemented in computer algebra systems and interactive proof assistants. This is done by implementing and verifying efficient algorithms using the Coq proof assistant together with the SSReflect extension. LÄS MER