Logical Environments

Capa
Gerard Huet, Gordon Plotkin
Cambridge University Press, 16 de set de 1993 - 338 páginas
0 Resenhas
Logical environments are computer systems that provide engineers and mathematicians with facilities to develop formal proofs. They also give some reasoning assistance and manage a data base of axiomatisations and theorems. Applications include both software and hardware certification. The design of such environments is an active research topic, at the frontier between mathematical logic and software engineering. Research ranges from abstract speculations about the foundations of mathematics, to very concrete considerations about ergonomic tools for building user interfaces with current workstation technology. New ideas in Type Theory may be put to use in a new generation of proof assistants taking advantage of uniform structures for the representation of mathematical and logical data. European Computer Science is specially active in this promising area, whose progress is crucial for safety-critical computer applications. The present volume is a selection of papers from research centres in Europe and the USA; together they give an overview of recent progress in the area.
 

O que estão dizendo - Escrever uma resenha

Não encontramos nenhuma resenha nos lugares comuns.

Conteúdo

David A Basin and Robert L Constable
15
Experience with FS0 as a Framework Theory
61
Logical Support for Modularisation
83
Algorithms for Logical Environments
131
A Canonical Calculus of Residuals
147
OrderSorted Polymorphism in Isabella
164
Logical Issues
189
Witness Extraction in Classical Logic through Normalization
219
ChurchRosser Property in Classical Free Deduction
273
Experiments
297
A Machine Checked Proof that Ackermanns Function
317
Direitos autorais

Termos e frases comuns

Referências a este livro

Informações bibliográficas