XINFORMAÇÕES SOBRE DIREITOS AUTORAIS
As obras disponibilizadas nesta Biblioteca Digital foram publicadas sob expressa autorização dos respectivos autores, em conformidade com a Lei 9610/98.
A consulta aos textos, permitida por seus respectivos autores, é livre, bem como a impressão de trechos ou de um exemplar completo exclusivamente para uso próprio. Não são permitidas a impressão e a reprodução de obras completas com qualquer outra finalidade que não o uso próprio de quem imprime.
A reprodução de pequenos trechos, na forma de citações em trabalhos de terceiros que não o próprio autor do texto consultado,é permitida, na medida justificada para a compreeensão da citação e mediante a informação, junto à citação, do nome do autor do texto original, bem como da fonte da pesquisa.
A violação de direitos autorais é passível de sanções civis e penais.
As obras disponibilizadas nesta Biblioteca Digital foram publicadas sob expressa autorização dos respectivos autores, em conformidade com a Lei 9610/98.
A consulta aos textos, permitida por seus respectivos autores, é livre, bem como a impressão de trechos ou de um exemplar completo exclusivamente para uso próprio. Não são permitidas a impressão e a reprodução de obras completas com qualquer outra finalidade que não o uso próprio de quem imprime.
A reprodução de pequenos trechos, na forma de citações em trabalhos de terceiros que não o próprio autor do texto consultado,é permitida, na medida justificada para a compreeensão da citação e mediante a informação, junto à citação, do nome do autor do texto original, bem como da fonte da pesquisa.
A violação de direitos autorais é passível de sanções civis e penais.
Coleção Digital
Título: EXTRACTION OF COMPUTATIONAL CONTENTS FROM INTUITIONIST PROOFS Autor: GEIZA MARIA HAMAZAKI DA SILVA
Instituição: PONTIFÍCIA UNIVERSIDADE CATÓLICA DO RIO DE JANEIRO - PUC-RIO
Colaborador(es):
EDWARD HERMANN HAEUSLER - ADVISOR
Nº do Conteudo: 5443
Catalogação: 10/09/2004 Idioma(s): PORTUGUESE - BRAZIL
Tipo: TEXT Subtipo: THESIS
Natureza: SCHOLARLY PUBLICATION
Nota: Todos os dados constantes dos documentos são de inteira responsabilidade de seus autores. Os dados utilizados nas descrições dos documentos estão em conformidade com os sistemas da administração da PUC-Rio.
Referência [pt]: https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=5443@1
Referência [en]: https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=5443@2
Referência DOI: https://doi.org/10.17771/PUCRio.acad.5443
Resumo:
Título: EXTRACTION OF COMPUTATIONAL CONTENTS FROM INTUITIONIST PROOFS Autor: GEIZA MARIA HAMAZAKI DA SILVA
Nº do Conteudo: 5443
Catalogação: 10/09/2004 Idioma(s): PORTUGUESE - BRAZIL
Tipo: TEXT Subtipo: THESIS
Natureza: SCHOLARLY PUBLICATION
Nota: Todos os dados constantes dos documentos são de inteira responsabilidade de seus autores. Os dados utilizados nas descrições dos documentos estão em conformidade com os sistemas da administração da PUC-Rio.
Referência [pt]: https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=5443@1
Referência [en]: https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=5443@2
Referência DOI: https://doi.org/10.17771/PUCRio.acad.5443
Resumo:
One of the main problems in computer science is to assure
that programs are implemented in such a way that they
satisfy a given specification. There are many studies about
methods to prove correctness of programs. This work
presents a method, belonging to the constructive synthesis
or proofs-as-programs paradigm, that comes from the Curry-
Howard isomorphism and extracts the computational contents
of intuitionist proofs. The synthesis process proposed
produces a program in an imperative language from a proof
in many-sorted intuitionist logic, where the axioms define
the abstract data types using Natural Deduction as
deductive system. It is proved the correctness, as well as
the completeness of the method regarding the Heyting
arithmetic with ômega-rule(in its computational version). A
discussion about the use of the finitary induction instead
of computational ômega-rule concludes the work.
Descrição | Arquivo |
COVER, ACKNOWLEDGEMENTS, RESUMO, ABSTRACT, SUMMARY AND LISTS | |
CHAPTER 1 | |
CHAPTER 2 | |
CHAPTER 3 | |
CHAPTER 4 | |
CHAPTER 5 | |
CHAPTER 6 | |
BIBLIOGRAPHY AND APPENDICES |