@conference {810,
	title = {Galois: A Language for Proofs Using Galois Connections and Fork Algebras},
	booktitle = { PLMMS{\textquoteright}09 - ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems},
	year = {2009},
	month = {August},
	address = {Munich, Germany},
	abstract = {<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>
},
	attachments = {https://haslab.uminho.pt/sites/default/files/pfsilva/files/plmms09.pdf},
	author = {Paulo Silva and Joost Visser and Jos{\'e} Nuno Oliveira}
}