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.
David A Basin and Robert L Constable
Experience with FS0 as a Framework Theory
Logical Support for Modularisation
Algorithms for Logical Environments
A Canonical Calculus of Residuals
OrderSorted Polymorphism in Isabella
Witness Extraction in Classical Logic through Normalization
ChurchRosser Property in Classical Free Deduction
A Machine Checked Proof that Ackermanns Function
abstract abstractor algebra algorithm application atomic axioms Calculus of Constructions cand classical proofs Computer Science conservative extension consider constructor corresponding Craig Interpolation defined denote derivation distributive law elements encoding equality equational logic equivalent example expression F h a filling-up rules finite formal formula framework logic free deduction functional types functor Harrop Harrop formula higher order higher-order implementation inclusion system induction hypothesis inductive definitions inductive predicates institution introduce intuitionistic Joseph Goguen labeling lambda lambda calculus LEGO lemma Logical Frameworks logical systems Martin-Lof's mathematical modules morphism natural deduction natural numbers notation notion Nuprl occurrences operations order logic origin function paper Post system Prawitz primitive recursive functions Prop properties propositions provable pushouts redex reduction rules relation result S-expressions semantics sequent sequent calculus Set Theory signature sort specification strong normalization structure syntactic syntax t-primitive term tion tuple type system type theory unification variables
Electronic Information and Communication in Mathematics: ICM 2002 ...
Visualização parcial - 2003