scientific article; zbMATH DE number 4191621
From MaRDI portal
Recommendations
Cited in
(30)- Checking algorithms for Pure Type Systems
- A higher-order calculus and theory abstraction
- scientific article; zbMATH DE number 1927418 (Why is no real title available?)
- I got plenty o' nuttin'
- From constructivism to computer science
- Canonicity of weak \(\omega\)-groupoid laws using parametricity theory
- Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics
- Modal dependent type theory and dependent right adjoints
- Coquand's calculus of constructions: A mathematical foundation for a proof development system
- Closure under alpha-conversion
- A short and flexible proof of strong normalization for the calculus of constructions
- An extended type system with lambda-typed lambda-expressions
- The extended calculus of constructions (ECC) with inductive types
- scientific article; zbMATH DE number 5033848 (Why is no real title available?)
- Termination checking with types
- Implementing type theory in higher order constraint logic programming
- Elimination of extensionality in Martin-Löf type theory
- A framework for defining logical frameworks
- scientific article; zbMATH DE number 591911 (Why is no real title available?)
- Metacircularity in the polymorphic \(\lambda\)-calculus
- Type checking with universes
- Using typed lambda calculus to implement formal systems on a machine
- Type theory as a foundation for computer science
- On the proof theory of Coquand's calculus of constructions
- Tactics and parameters
- Bridging Curry and Church's typing style
- Variants of the basic calculus of constructions
- Higher-order substitutions
- Logic of refinement types
- Unification with extended patterns
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)
