Proof assistance for refnement in type theory
Visualitza/Obre
Estadístiques de LA Referencia / Recolecta
Inclou dades d'ús des de 2022
Cita com:
hdl:2117/95873
Tipus de documentReport de recerca
Data publicació2003-03-02
Condicions d'accésAccés obert
Tots els drets reservats. Aquesta obra està protegida pels drets de propietat intel·lectual i
industrial corresponents. Sense perjudici de les exempcions legals existents, queda prohibida la seva
reproducció, distribució, comunicació pública o transformació sense l'autorització del titular dels drets
Abstract
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.
Forma partR00-19
Col·leccions
Fitxers | Descripció | Mida | Format | Visualitza |
---|---|---|---|---|
R00-19.pdf | 199,7Kb | Visualitza/Obre |