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