Carregant...
Carregant...

Vés al contingut (premeu Retorn)

Proof assistance for refnement in type theory

Autor
Mylonakis, N.
Tipus d'activitat
Document cientificotècnic
Data
2003-03-02
Codi
R00-19
Repositori
http://hdl.handle.net/2117/95873 Obrir en finestra nova
Resum
In this paper, we represent in type theory a proof system for refinement of algebraic specifications. . The representation is not adequate but full because the use of proof obligations to represent side-conditions. Using this representation, we can develop a proof tactic to help the development of proofs of refinement.
Citació
Mylonakis, N. "Proof assistance for refnement in type theory". 2003.
Paraules clau
Proof assistance, Refinement of algebraic specifications, Type theory

Participants

Arxius