scientific article; zbMATH DE number 591911
From MaRDI portal
Publication:4296744
zbMath0823.68101MaRDI QIDQ4296744
Publication date: 20 June 1994
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Logic in artificial intelligence (68T27) General topics in artificial intelligence (68T01)
Related Items (41)
Selectional restrictions, types and categories ⋮ Computational adequacy for recursive types in models of intuitionistic set theory ⋮ Parametric Church's thesis: synthetic computability without choice ⋮ Representing inductively defined sets by wellorderings in Martin-Löf's type theory ⋮ Propositional forms of judgemental interpretations ⋮ The metatheory of UTT ⋮ On extensibility of proof checkers ⋮ Encoding Z-style Schemas in type theory ⋮ Proof Assistants for Natural Language Semantics ⋮ Coercions in a polymorphic type system ⋮ Pure type systems with explicit substitutions ⋮ Eliminating dependent pattern matching without K ⋮ Structural subtyping for inductive types with functorial equality rules ⋮ Denotational semantics for guarded dependent type theory ⋮ Hoare type theory, polymorphism and separation ⋮ Type theoretic semantics for SemNet ⋮ Composition of deductions within the propositions-as-types paradigm ⋮ 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 ⋮ Adjectival and adverbial modification: the view from modern type theories ⋮ Conditionally reversible computations and weak universality in category theory ⋮ Natural language inference in Coq ⋮ Semantics of constructions. I: The traditional approach ⋮ Remarks on Isomorphisms of Simple Inductive Types ⋮ An experimental library of formalized Mathematics based on the univalent foundations ⋮ Transitivity in coercive subtyping ⋮ Coercion completion and conservativity in coercive subtyping ⋮ An induction principle for pure type systems ⋮ N. G. de Bruijn's contribution to the formalization of mathematics ⋮ Automorphisms of types and their applications ⋮ Manifest Fields and Module Mechanisms in Intensional Type Theory ⋮ A pluralist approach to the formalisation of mathematics ⋮ A minimalist two-level foundation for constructive mathematics ⋮ Equilogical spaces ⋮ ETA-RULES IN MARTIN-LÖF TYPE THEORY ⋮ Search algorithms in type theory ⋮ The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type ⋮ Automorphisms of types in certain type theories and representation of finite groups ⋮ Encoding FIX in Object Calculi
Uses Software
This page was built for publication:
