scientific article; zbMATH DE number 4191621

zbMATH Open0723.03034MaRDI QIDQ3211296FDOQ3211296

Authors: Zhaohui Luo 

Publication date: 1989

Title of this publication is not available (Why is that?)

Recommendations

• The extended calculus of constructions (ECC) with inductive types
• scientific article; zbMATH DE number 1405632
• A higher-order calculus and theory abstraction
• scientific article; zbMATH DE number 591911
• The calculus of constructions

zbMATH Keywords

higher-order calculusECCextension of the calculus of constructionsfully cumulative type hierarchystrong sum types

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Combinatory logic and lambda calculus (03B40) Second- and higher-order arithmetic and fragments (03F35)

Cited In (30)

• Title not available (Why is that?)
• Title not available (Why is that?)
• Termination checking with types
• Title not available (Why is that?)
• Canonicity of weak \(\omega\)-groupoid laws using parametricity theory
• A framework for defining logical frameworks
• Variants of the basic calculus of constructions
• Unification with extended patterns
• Title not available (Why is that?)
• From constructivism to computer science
• Type theory as a foundation for computer science
• The extended calculus of constructions (ECC) with inductive types
• Logic of refinement types
• I Got Plenty o’ Nuttin’
• Higher-order substitutions
• Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics
• Tactics and Parameters
• Bridging Curry and Church's typing style
• Closure under alpha-conversion
• A short and flexible proof of strong normalization for the calculus of constructions
• Metacircularity in the polymorphic \(\lambda\)-calculus
• Type checking with universes
• Checking algorithms for Pure Type Systems
• Implementing type theory in higher order constraint logic programming
• Modal dependent type theory and dependent right adjoints
• Coquand's calculus of constructions: A mathematical foundation for a proof development system
• Using typed lambda calculus to implement formal systems on a machine
• Elimination of extensionality in Martin-Löf type theory
• A higher-order calculus and theory abstraction
• On the proof theory of Coquand's calculus of constructions

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3211296)