Introduction to generalized type systems
From MaRDI portal
Publication:4939697
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
(46)- Applications of type theory
- Checking algorithms for Pure Type Systems
- Type-specialized staged programming with process separation
- Pedagogical lambda-cube: the \(\lambda^{2}\) case
- Strong normalization in type systems: A model theoretical approach
- Term-Generic Logic
- scientific article; zbMATH DE number 1231611 (Why is no real title available?)
- The undecidability of pattern matching in calculi where primitive recursive functions are representable
- Typed $\lambda$-calculi with one binder
- Higher-order pattern anti-unification in linear time
- scientific article; zbMATH DE number 960927 (Why is no real title available?)
- Modularity of termination and confluence in combinations of rewrite systems with \(\lambda_\omega\)
- Unified syntax with iso-types
- The expansion postponement in pure type systems
- \(\eta\)-equivalence in core dependent Haskell
- On functions and types: a tutorial
- The variable containment problem
- Proof certificates for equality reasoning
- Executable relational specifications of polymorphic type systems using Prolog
- scientific article; zbMATH DE number 7204440 (Why is no real title available?)
- The calculus of constructions as a framework for proof search with set variable instantiation
- A Rewriting Logic Approach to Type Inference
- Comprehensive Parametric Polymorphism: Categorical Models and Type Theory
- A typed \(\lambda\)-calculus for proving-by-example and bottom-up generalization procedure
- The Girard-Reynolds isomorphism (second edition)
- scientific article; zbMATH DE number 7561487 (Why is no real title available?)
- \textsc{LeoPARD} -- a generic platform for the implementation of higher-order reasoners
- An induction principle for pure type systems
- Closure under alpha-conversion
- An extended type system with lambda-typed lambda-expressions
- Representing proof transformations for program optimization
- An algorithm for checking incomplete proof objects in type theory with localization and unification
- A note on the proof theory of the \(\lambda \Pi\)-calculus
- Mechanized metatheory revisited
- scientific article; zbMATH DE number 1692907 (Why is no real title available?)
- Specifying type systems
- Type theories from Barendregt's cube for theorem provers
- Comparing cubes of typed and type assignment systems
- An intuitionistic set-theoretical model of fully dependent CC
- The Girard-Reynolds isomorphism
- Classical \(F_{\omega}\), orthogonality and symmetric candidates
- A unified approach to type theory through a refined \(\lambda\)-calculus
- A semantic framework for proof evidence
- A syntactic proof of the conservativity of \(\lambda_\omega\) over \(\lambda_2\)
- scientific article; zbMATH DE number 177773 (Why is no real title available?)
- Singleton, union and intersection types for program extraction
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)
