scientific article; zbMATH DE number 591911
From MaRDI portal
Publication:4296744
Recommendations
Cited in
(54)- Encoding Z-style Schemas in type theory
- Composition of deductions within the propositions-as-types paradigm
- Gradability in MTT-Semantics
- A minimalist two-level foundation for constructive mathematics
- Eliminating dependent pattern matching without K
- Adjectival and adverbial modification: the view from modern type theories
- Automorphisms of types in certain type theories and representation of finite groups
- Congruence types
- History and philosophy of constructive type theory
- Synthetic domain theory in type theory: another logic of computable functions
- Conditionally reversible computations and weak universality in category theory
- Manifest Fields and Module Mechanisms in Intensional Type Theory
- scientific article; zbMATH DE number 4191621 (Why is no real title available?)
- Selectional restrictions, types and categories
- On extensibility of proof checkers
- Coercion completion and conservativity in coercive subtyping
- Topological quantum gates in homotopy type theory
- Computational adequacy for recursive types in models of intuitionistic set theory
- An induction principle for pure type systems
- Proof assistants for natural language semantics
- scientific article; zbMATH DE number 53088 (Why is no real title available?)
- scientific article; zbMATH DE number 2248154 (Why is no real title available?)
- Type theory as a foundation for computer science
- The extended calculus of constructions (ECC) with inductive types
- The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type
- A two-level approach towards lean proof-checking
- Propositional forms of judgemental interpretations
- Natural language inference in Coq
- Encoding FIX in Object Calculi
- N. G. de Bruijn's contribution to the formalization of mathematics
- The metatheory of UTT
- Pure type systems with explicit substitutions
- Transitivity in coercive subtyping
- Parametric Church's thesis: synthetic computability without choice
- Eta-rules in Martin-Löf type theory
- Structural subtyping for inductive types with functorial equality rules
- Search algorithms in type theory
- Equilogical spaces
- Type theoretic semantics for SemNet
- Treatise on intuitionistic type theory
- A pluralist approach to the formalisation of mathematics
- Coercions in a polymorphic type system
- Denotational semantics for guarded dependent type theory
- Semantics of constructions. I: The traditional approach
- Representing inductively defined sets by wellorderings in Martin-Löf's type theory
- Computations on types
- Automating inversion of inductive predicates in Coq
- Automorphisms of types and their applications
- Remarks on isomorphisms of simple inductive types
- Implicit coercions in type systems
- Hoare type theory, polymorphism and separation
- A higher-order calculus and theory abstraction
- Modular properties of algebraic type systems
- An experimental library of formalized mathematics based on the univalent foundations
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 Q4296744)
