<?xml version="1.0" encoding="UTF-8"?><xml><records><record><source-app name="Biblio" version="6.x">Drupal-Biblio</source-app><ref-type>47</ref-type><contributors><authors><author><style face="normal" font="default" size="100%">Paulo Silva</style></author><author><style face="normal" font="default" size="100%">Joost Visser</style></author><author><style face="normal" font="default" size="100%">José Nuno Oliveira</style></author></authors></contributors><titles><title><style face="normal" font="default" size="100%">Galois: A Language for Proofs Using Galois Connections and Fork Algebras</style></title><secondary-title><style face="normal" font="default" size="100%"> PLMMS'09 - ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems</style></secondary-title></titles><dates><year><style  face="normal" font="default" size="100%">2009</style></year><pub-dates><date><style  face="normal" font="default" size="100%">August</style></date></pub-dates></dates><urls><related-urls><url><style face="normal" font="default" size="100%">https://haslab.uminho.pt/sites/default/files/pfsilva/files/plmms09.pdf</style></url></related-urls></urls><pub-location><style face="normal" font="default" size="100%">Munich, Germany</style></pub-location><abstract><style face="normal" font="default" size="100%">&lt;p&gt;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.&lt;/p&gt;
&lt;p&gt;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.&lt;/p&gt;
</style></abstract></record></records></xml>