scientific article
From MaRDI portal
Publication:3211296
zbMath0723.03034MaRDI QIDQ3211296
Publication date: 1989
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
higher-order calculusECCextension of the calculus of constructionsfully cumulative type hierarchystrong sum types
Symbolic computation and algebraic computation (68W30) Second- and higher-order arithmetic and fragments (03F35) Combinatory logic and lambda calculus (03B40)
Related Items
Canonicity of weak \(\omega\)-groupoid laws using parametricity theory, Variants of the basic calculus of constructions, A higher-order calculus and theory abstraction, I Got Plenty o’ Nuttin’, Bridging Curry and Church's typing style, Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics, Type theory as a foundation for computer science, Checking algorithms for Pure Type Systems, Logic of refinement types, Elimination of extensionality in Martin-Löf type theory, Closure under alpha-conversion, A short and flexible proof of strong normalization for the calculus of constructions, Type checking with universes, Metacircularity in the polymorphic \(\lambda\)-calculus, The extended calculus of constructions (ECC) with inductive types, Coquand's calculus of constructions: A mathematical foundation for a proof development system, Using typed lambda calculus to implement formal systems on a machine, Termination checking with types, Tactics and Parameters, On the proof theory of Coquand's calculus of constructions, Modal dependent type theory and dependent right adjoints, From constructivism to computer science, Unification with extended patterns, Implementing type theory in higher order constraint logic programming, Unnamed Item, Higher-order substitutions, A Framework for Defining Logical Frameworks
