scientific article; zbMATH DE number 591911
From MaRDI portal
Publication:4296744
zbMATH Open0823.68101MaRDI QIDQ4296744FDOQ4296744
Authors: Zhaohui Luo 
Publication date: 20 June 1994
Title of this publication is not available (Why is that?)
Recommendations
Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Logic in artificial intelligence (68T27) General topics in artificial intelligence (68T01)
Cited In (54)
- Composition of deductions within the propositions-as-types paradigm
- Eliminating dependent pattern matching without K
- A minimalist two-level foundation for constructive mathematics
- Adjectival and adverbial modification: the view from modern type theories
- Congruence types
- Automorphisms of types in certain type theories and representation of finite groups
- Synthetic domain theory in type theory: another logic of computable functions
- History and philosophy of constructive type theory
- Conditionally reversible computations and weak universality in category theory
- Manifest Fields and Module Mechanisms in Intensional Type Theory
- Title not available (Why is that?)
- On extensibility of proof checkers
- Coercion completion and conservativity in coercive subtyping
- Selectional restrictions, types and categories
- Topological quantum gates in homotopy type theory
- An induction principle for pure type systems
- Computational adequacy for recursive types in models of intuitionistic set theory
- Title not available (Why is that?)
- Title not available (Why is that?)
- Proof assistants for natural language semantics
- 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
- The extended calculus of constructions (ECC) with inductive types
- A two-level approach towards lean proof-checking
- Propositional forms of judgemental interpretations
- Encoding FIX in Object Calculi
- Natural language inference in Coq
- The metatheory of UTT
- Pure type systems with explicit substitutions
- N. G. de Bruijn's contribution to the formalization of mathematics
- 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
- Denotational semantics for guarded dependent type theory
- Coercions in a polymorphic type system
- Semantics of constructions. I: The traditional approach
- Representing inductively defined sets by wellorderings in Martin-Löf's type theory
- Automating inversion of inductive predicates in Coq
- Computations on types
- Automorphisms of types and their applications
- Remarks on isomorphisms of simple inductive types
- Implicit coercions in type systems
- Modular properties of algebraic type systems
- An experimental library of formalized mathematics based on the univalent foundations
- Hoare type theory, polymorphism and separation
- A higher-order calculus and theory abstraction
- Encoding Z-style Schemas in type theory
- Gradability in MTT-Semantics
Uses Software
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)
