scientific article; zbMATH DE number 65534
From MaRDI portal
Publication:4012882
Recommendations
- Foundations of Software Science and Computational Structures
- Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory
- Pure type system conversion is always typable
- Normalization by Evaluation for Martin-Löf Type Theory with One Universe
- On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory
Cited in
(34)- Type inference for pure type systems
- A linear logical framework
- Typed operational semantics for higher-order subtyping.
- Alpha-conversion and typability
- A note on the proof theory of the -calculus
- An adequacy theorem for dependent type theory
- Formal metatheory of the lambda calculus using Stoughton's substitution
- Types for modules
- Formalizing adequacy: a case study for higher-order abstract syntax
- Canonicity and normalization for dependent type theory
- Decidability for non-standard conversions in typed lambda-calculi
- A representation of \(F_{\omega}\) in LF
- A meta linear logical framework
- A modular type-checking algorithm for type theory with singleton types and proof irrelevance
- Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory
- A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance
- An algorithm for checking incomplete proof objects in type theory with localization and unification
- Higher-order superposition for dependent types
- Categorical reconstruction of a reduction free normalization proof
- A cubical language for Bishop sets
- Dependent Types at Work
- Formalisation in constructive type theory of Stoughton's substitution for the lambda calculus
- Foundations of Software Science and Computational Structures
- The metatheory of UTT
- Big step normalisation for type theory
- \(\eta\)-equivalence in core dependent Haskell
- The Alf proof editor and its proof engine
- Closure under alpha-conversion
- A typed -calculus for proving-by-example and bottom-up generalization procedure
- Design and implementation of the andromeda proof assistant
- Explicit substitutions for contextual type theory
- Implementing a type theory with observational equality, using normalisation by evaluation
- Two algorithms in search of a type-system
- Analytic proof systems for -calculus: the elimination of transitivity, and why it matters
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 Q4012882)
