Recommendations
- Introduction to Type Theory
- scientific article; zbMATH DE number 960927
- scientific article; zbMATH DE number 4126684
- scientific article; zbMATH DE number 827981
- Types for Proofs and Programs
- Specifying type systems
- Generative type abstraction and type-level computation
- scientific article; zbMATH DE number 1302061
- A new look at generalized rewriting in type theory
- Type inference for pure type systems
Cited in
(54)- The undecidability of pattern matching in calculi where primitive recursive functions are representable
- A syntactic proof of the conservativity of \(\lambda_\omega\) over \(\lambda_2\)
- A unified approach to type theory through a refined -calculus
- Comparing cubes of typed and type assignment systems
- The expansion postponement in pure type systems
- The calculus of constructions as a framework for proof search with set variable instantiation
- A semantic framework for proof evidence
- Proof certificates for equality reasoning
- The Girard-Reynolds isomorphism
- Strong normalization in type systems: A model theoretical approach
- A note on the proof theory of the -calculus
- Type-specialized staged programming with process separation
- Mechanized metatheory revisited
- Higher-order pattern anti-unification in linear time
- Classical \(F_{\omega}\), orthogonality and symmetric candidates
- scientific article; zbMATH DE number 1692907 (Why is no real title available?)
- Executable relational specifications of polymorphic type systems using Prolog
- Comprehensive Parametric Polymorphism: Categorical Models and Type Theory
- Specifying type systems
- On functions and types: a tutorial
- Unified syntax with iso-types
- A Rewriting Logic Approach to Type Inference
- Term-Generic Logic
- \textsc{LeoPARD} -- a generic platform for the implementation of higher-order reasoners
- scientific article; zbMATH DE number 177773 (Why is no real title available?)
- scientific article; zbMATH DE number 1231611 (Why is no real title available?)
- scientific article; zbMATH DE number 1342247 (Why is no real title available?)
- scientific article; zbMATH DE number 1499110 (Why is no real title available?)
- Modularity of termination and confluence in combinations of rewrite systems with _
- The variable containment problem
- An algorithm for checking incomplete proof objects in type theory with localization and unification
- Applications of type theory
- A simpler undecidability proof for system F inhabitation
- Singleton, union and intersection types for program extraction
- scientific article; zbMATH DE number 7204440 (Why is no real title available?)
- An extended type system with lambda-typed lambda-expressions
- Representing proof transformations for program optimization
- Type theories from Barendregt's cube for theorem provers
- Pedagogical lambda-cube: the \(\lambda^{2}\) case
- On cubism
- scientific article; zbMATH DE number 960927 (Why is no real title available?)
- Typed \lambda-calculi with one binder
- An induction principle for pure type systems
- \(\eta\)-equivalence in core dependent Haskell
- Checking algorithms for Pure Type Systems
- Closure under alpha-conversion
- An intuitionistic set-theoretical model of fully dependent CC
- A typed -calculus for proving-by-example and bottom-up generalization procedure
- Finite combinatory logic with predicates
- Second-order generalised algebraic theories: signatures and first-order semantics
- Equivalence of eval-readback and eval-apply big-step evaluators by structuring the lambda-calculus's strategy space
- From proof-theoretic validity to base-extension semantics for intuitionistic propositional logic
- Title not available (Why is no real title available?)
- The Girard-Reynolds isomorphism (second edition)
This page was built for publication: Introduction to generalized type systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4939697)
