UID:
almafu_9960119451502883
Format:
1 online resource (xii, 403 pages) :
,
digital, PDF file(s).
ISBN:
0-511-56980-7
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.
Note:
Title from publisher's bibliographic system (viewed on 05 Oct 2015).
,
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.
,
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.
,
English
Additional Edition:
ISBN 0-521-41300-1
Language:
English
URL:
https://doi.org/10.1017/CBO9780511569807
