Format:
1 Online-Ressource (xii, 403 pages)
,
digital, PDF file(s)
ISBN:
9780511569807
Content:
This 1991 volume contains the proceedings of the first international workshop on Logical Frameworks. The contributions are concerned with the application of logical reasoning and proof theory in computer science and its relevance to automatic theorem proving, and consequently topics such as artificial intelligence. It is the only source for much of this material and will be a necessary purchase for mathematicians and computer scientists undertaking research at the interface of logic and software engineering
Content:
Inductive sets and families in Martin-Löf's type theory and their set-theoretic semantics / Peter Dybjer -- Proof-search in the [lambda][pi]-calculus / David Pym and Lincoln Wallen -- Finding computational content in classical proofs / Robert Constable and Chet Murthy -- Models of partial inductive definitions / Lars Hallnäs -- Structural frameworks, substructural logics, and the role of elimination inferences / Peter Schroeder-Heister
Content:
Two frameworks of theories and their implementation in Isabelle / Peter Aczel, David P. Carlisle and Nax Mendler -- A plea for weaker frameworks / N.G. de Bruijn -- Nederpelt's calculus extended with a notion of context as a logical framework / Philippe de Groote -- The Boyer-Moore prover and Nuprl : an experimental comparison / David Basin and Matt Kaufmann -- Goal directed proof construction in type theory / L. Helmink and R.M.C. Ahn -- Logic programming in the LF logical framework / Frank Pfenning -- Operational semantics in a natural deduction setting / Rod Burstall and Furio Honsell -- Encoding dependent types in an intuitionistic logic / Amy Felty -- An algorithm for testing conversion in type theory / Thierry Coquand
Note:
Title from publisher's bibliographic system (viewed on 05 Oct 2015)
Additional Edition:
ISBN 9780521413008
Additional Edition:
Erscheint auch als Druck-Ausgabe ISBN 9780521413008
Language:
English
DOI:
10.1017/CBO9780511569807
