On the unification problem for Cartesian closed categories
DOI10.2307/2275552zbMATH Open0882.03044OpenAlexW2051020081MaRDI QIDQ4358059FDOQ4358059
Authors: Paliath Narendran, Frank Pfenning, Richard Statman 
Publication date: 1997
Published in: Journal of Symbolic Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.2307/2275552
Recommendations
- Univalence in locally Cartesian closed categories
- scientific article; zbMATH DE number 4108981
- scientific article; zbMATH DE number 540506
- On the unicity of the theory of higher categories
- scientific article; zbMATH DE number 940753
- Cartesian closed extensions of the category of uniform spaces
- scientific article; zbMATH DE number 1284147
- Unification properties of commutative theories: a categorical treatment
- scientific article; zbMATH DE number 3968855
- scientific article; zbMATH DE number 3961917
matchingNP-completeCartesian closed categoriesundecidabilityunification problemsemantics of programming languagesunification modulo the linear isomorphisms
Analysis of algorithms and problem complexity (68Q25) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15) Semantics in the theory of computing (68Q55) Undecidability and degrees of sets of sentences (03D35)
Cites Work
- Title not available (Why is that?)
- A Unification Algorithm for Associative-Commutative Functions
- Complete Sets of Reductions for Some Equational Theories
- Complexity of unification problems with associative-commutative operators
- Retrieving library functions by unifying types modulo linear isomorphism
- Completion of a Set of Rules Modulo a Set of Equations
- Using types as search keys in function libraries
- Associative-commutative unification
- Provable isomorphisms of types
- The category of finite sets and Cartesian closed categories
Cited In (8)
- Univalence in locally Cartesian closed categories
- Unification modulo homomorphic encryption
- Unification modulo homomorphic encryption
- Title not available (Why is that?)
- Unification and matching modulo nilpotence
- An algorithm for distributive unification
- Retrieving library functions by unifying types modulo linear isomorphism
- Automated verification of equivalence properties of cryptographic protocols
This page was built for publication: On the unification problem for Cartesian closed categories
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4358059)
