ScienceOpen:
research and publishing network
For Publishers
Discovery
Metadata
Peer review
Hosting
Publishing
For Researchers
Join
Publish
Review
Collect
My ScienceOpen
Sign in
Register
Dashboard
Blog
About
Search
Advanced search
My ScienceOpen
Sign in
Register
Dashboard
Search
Search
Advanced search
For Publishers
Discovery
Metadata
Peer review
Hosting
Publishing
For Researchers
Join
Publish
Review
Collect
Blog
About
33
views
0
references
Top references
cited by
14
Cite as...
0 reviews
Review
0
comments
Comment
0
recommends
+1
Recommend
0
collections
Add to
0
shares
Share
Twitter
Sina Weibo
Facebook
Email
1,191
similar
All similar
Record
: found
Abstract
: not found
Book Chapter
: not found
Logical Frameworks
An algorithm for testing conversion in type theory
edited_book
Author(s):
Thierry Coquand
Publication date:
September 26 1991
Publisher:
Cambridge University Press
Read this book at
Publisher
Buy book
Review
Review book
Invite someone to review
Bookmark
Cite as...
There is no author summary for this book yet. Authors can add summaries to their books on ScienceOpen to make them more accessible to a non-specialist audience.
Related collections
Numerical Algebra, Matrix Theory, Differential-Algebraic Equations, and Control Theory
Author and book information
Book Chapter
Publication date:
September 26 1991
Pages
: 255-279
DOI:
10.1017/CBO9780511569807.011
SO-VID:
10691ec3-6d23-4212-8d06-1a9e805013ba
History
Data availability:
Comments
Comment on this book
Sign in to comment
Book chapters
pp. 40
A plea for weaker frameworks
pp. 89
The Boyer-Moore prover and Nuprl: an experimental comparison
pp. 120
Goal directed proof construction in type theory
pp. 149
Logic programming in the LF logical framework
pp. 185
Operational semantics in a natural deduction setting
pp. 215
Encoding dependent types in an intuitionistic logic
pp. 255
An algorithm for testing conversion in type theory
pp. 280
Inductive sets and families in Martin-Löf's type theory and their set-theoretic semantics
pp. 309
Proof-search in the λΠ-calculus
pp. 341
Finding computational content in classical proofs
pp. 385
Structural frameworks, substructural logics, and the role of elimination inferences
Similar content
1,191
A hybrid PSO–BFO evolutionary algorithm for optimization of fused deposition modelling process parameters
Authors:
Maraboina Raju
,
Munish Kumar Gupta
,
Neeraj Bhanot
…
Myocardial tagging by Cardiovascular Magnetic Resonance: evolution of techniques--pulse sequences, analysis algorithms, and applications
Authors:
El-Sayed H. Ibrahim
A New Treatment Algorithm That Incorporates Minimally Invasive Surgery for Pyogenic Spondylodiscitis in the Thoracic and Lumbar Spines: The Results of Its Clinical Application to a Series of 34 Patients.
Authors:
Yoichi Tani
,
Takanori Saito
,
Shinichiro Taniguchi
…
See all similar
Cited by
14
A general formulation of simultaneous inductive-recursive definitions in type theory
Authors:
Peter Dybjer
The Alf proof editor and its proof engine
Authors:
Lena Magnusson
,
Bengt Nordström
Categorical reconstruction of a reduction free normalization proof
Authors:
Thorsten Altenkirch
,
Martin Hofmann
,
Thomas Streicher
See all cited by