On the proof theory of Coquand's calculus of constructions

Annals of Pure and Applied Logic 83 (1):23-101 (1997)
  Copy   BIBTEX

Abstract

This article has no associated abstract. (fix it)

Categories

Keywords

Reprint years

DOI

10.1016/s0168-0072(96)00008-5

Other Versions

original Seldin, Jonathan P. (1997) "We provide a simple and transparent construction of Hrushovski's strongly minimal fusions in the case where the fused strongly minimal sets are vector spaces. We strengthen Hrushovski's result by showing that the strongly minimal fusions are model complete". Annals of Pure and Applied Logic 83(1):23-101

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 100,793

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

2-Sequent calculus: a proof theory of modalities.Andrea Masini - 1992 - Annals of Pure and Applied Logic 58 (3):229-246.
Representation and duality of the untyped λ-calculus in nominal lattice and topological semantics, with a proof of topological completeness.Murdoch J. Gabbay & Michael Gabbay - 2017 - Annals of Pure and Applied Logic 168 (3):501-621.
Towards NP – P via proof complexity and search.Samuel R. Buss - 2012 - Annals of Pure and Applied Logic 163 (7):906-917.
Proof nets sequentialisation in multiplicative linear logic.Paolo Di Giamberardino & Claudia Faggian - 2008 - Annals of Pure and Applied Logic 155 (3):173-182.
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.
Algebraic proof theory: Hypersequents and hypercompletions.Agata Ciabattoni, Nikolaos Galatos & Kazushige Terui - 2017 - Annals of Pure and Applied Logic 168 (3):693-737.
Proof theory for lattice-ordered groups.Nikolaos Galatos & George Metcalfe - 2016 - Annals of Pure and Applied Logic 167 (8):707-724.

Analytics

Added to PP
2013-10-30

Downloads
45 (#473,051)

6 months
5 (#1,012,768)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Pure type systems with more liberal rules.Martin Bunder & Wil Dekkers - 2001 - Journal of Symbolic Logic 66 (4):1561-1580.

View all 7 citations / Add more citations

References found in this work

The formulæ-as-types notion of construction.W. A. Howard - 1995 - In Philippe De Groote (ed.), The Curry-Howard isomorphism. Louvain-la-Neuve: Academia.
A sequent calculus for type assignment.Jonathan P. Seldin - 1977 - Journal of Symbolic Logic 42 (1):11-28.
A tour of the multivariate lambda calculus.Garrel Pottinger - 1990 - In J. Dunn & A. Gupta (eds.), Truth or Consequences: Essays in Honor of Nuel Belnap. Boston, MA, USA: Kluwer Academic Publishers. pp. 209--229.

Add more references