%0 Conference Paper
%B PLMMS'09 - ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems
%D 2009
%T Galois: A Language for Proofs Using Galois Connections and Fork Algebras
%A Paulo Silva
%A Joost Visser
%A José Nuno Oliveira
%C Munich, Germany
%X <p>Galois is a domain specific language supported by the Galculator interactive proof-assistant prototype. Galculator uses an equational approach based on Galois connections with indirect equality as an additional inference rule. Galois allows for the specification of different theories in a point-free style by using fork algebras, an extension of relation algebras with expressive power of first-order logic. The language offers sub-languages to derive proof rules from Galois connections, to express proof tactics, and to organize axioms and theorems into modular definitions.</p> <p>In this paper, we describe how the algebraic theory underlying the proof-method drives the design of the Galois language. We provide the syntax and semantics of important fragments of Galois and show how they are hierarchically combined into a complete language.</p>
%8 August
%> https://haslab.uminho.pt/sites/default/files/pfsilva/files/plmms09.pdf