Interpreting HOL in the calculus of constructions

Journal of Applied Logic 2 (2):173-189 (2004)
  Copy   BIBTEX

Abstract

This article has no associated abstract. (fix it)

Categories

Keywords

Reprint years

DOI

10.1016/j.jal.2004.02.003

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 93,127

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

Review: J. Roger Hindley, Jonathan P. Seldin, Introduction to Combinators and $lambda$-Calculus. [REVIEW]J. L. Krivine - 1988 - Journal of Symbolic Logic 53 (3):985-986.
J. Roger Hindley and Jonathan P. Seldin. Introduction to combinators and λ-calculus. London Mathematical Society student texts, no. 1. Cambridge University Press, Cambridge etc. 1986, vi + 360 pp. [REVIEW]J. L. Krivine - 1988 - Journal of Symbolic Logic 53 (3):985-986.
Review: Haskell B. Curry, J. Roger Hindley, Jonathan P. Seldin, Combinatory Logic. [REVIEW]Henk Barendregt - 1977 - Journal of Symbolic Logic 42 (1):109-110.
Combinatory logic. Haskell B. Curry, J. Roger Hindley, and Jonathan P. Seldin. Combinatory logic. Volume II. Studies in logic and the foundations of mathematics, vol. 65. North-Holland Publishing Company, Amsterdam and London 1972, XIV + 520 pp. [REVIEW]Henk Barendregt - 1977 - Journal of Symbolic Logic 42 (1):109-110.
Variants of the basic calculus of constructions.M. W. Bunder & Jonathan P. Seldin - 2004 - Journal of Applied Logic 2 (2):191-217.
On the proof theory of Coquand's calculus of constructions.Jonathan P. Seldin - 1997 - Annals of Pure and Applied Logic 83 (1):23-101.
Error analysis of digital filters using HOL theorem proving.Behzad Akbarpour & Sofiène Tahar - 2007 - Journal of Applied Logic 5 (4):651-666.
Efficiently checking propositional refutations in HOL theorem provers.Tjark Weber & Hasan Amjad - 2009 - Journal of Applied Logic 7 (1):26-40.
Introduction to HOL: A Theorem Proving Environment for Higher Order Logic.Michael J. C. Gordon & Tom F. Melham - 1993
Formalised Cut Admissibility for Display Logic.Jeremy E. Dawson - unknown

Analytics

Added to PP
2016-06-30

Downloads
22 (#733,560)

6 months
3 (#1,046,015)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

The logic of choice.Andreas Blass & Yuri Gurevich - 2000 - Journal of Symbolic Logic 65 (3):1264-1310.
On the proof theory of Coquand's calculus of constructions.Jonathan P. Seldin - 1997 - Annals of Pure and Applied Logic 83 (1):23-101.

Add more references