Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/38932
Título: | 'Galculator': functional prototype of a Galois-connection based proof assistant |
Autor(es): | Silva, Paulo F. Oliveira, José Nuno Fonseca |
Palavras-chave: | Proof assistant Point-free notation Haskell Galois connections GADT DSL GAD |
Data: | 2008 |
Editora: | ACM |
Resumo(s): | Galculator is the name of the prototype of a proof assistant of a special brand: it is solely based on the algebra of Galois connections. When combined with the pointfree transform and tactics such as the indirect equality principle, Galois connections offer a very powerful, generic device to tackle the complexity of proofs in program verification. The paper describes the architecture of the current Galculator prototype, which is implemented in Haskell in order to steer types as much as possible. The prospect of integrating the Galculator with other proof assistants such as e.g. Coq is also discussed. |
Tipo: | Artigo em ata de conferência |
URI: | https://hdl.handle.net/1822/38932 |
ISBN: | 978-1-60558-117-0 |
DOI: | 10.1145/1389449.1389456 |
Versão da editora: | http://dl.acm.org/citation.cfm?doid=1389449.1389456 |
Arbitragem científica: | yes |
Acesso: | Acesso aberto |
Aparece nas coleções: |