| Coercive subtyping: theory and implementation Z Luo, S Soloviev, T Xue Information and Computation 223, 18-42, 2013 | 80 | 2013 |
| The genericity theorem and parametricity in the polymorphic λ-calculus G Longo, K Milsted, S Soloviev Theoretical computer science 121 (1-2), 323-349, 1993 | 65 | 1993 |
| Coercion completion and conservativity in coercive subtyping S Soloviev, Z Luo Annals of pure and applied logic 113 (1-3), 297-322, 2001 | 52 | 2001 |
| A logic of subtyping G Loop, K Milsted, S Soloviev Proceedings of Tenth Annual IEEE Symposium on Logic in Computer Science, 292-299, 1995 | 47 | 1995 |
| A complete axiom system for isomorphism of types in closed categories S Soloviev International Conference on Logic for Programming Artificial Intelligence …, 1993 | 47 | 1993 |
| Dependent coercions Z Luo, S Soloviev Electronic Notes in Theoretical Computer Science 29, 152-168, 1999 | 34 | 1999 |
| On the conditions of full coherence in closed categories SV Soloviev Journal of Pure and Applied Algebra 69 (3), 301-329, 1991 | 30 | 1991 |
| Proof of a conjecture of S. Mac Lane S Soloviev Annals of Pure and Applied Logic 90 (1-3), 101-162, 1997 | 27 | 1997 |
| Some algorithmic and proof-theoretical aspects of coercive subtyping A Jones, Z Luo, S Soloviev Types for Proofs and Programs: International Workshop TYPES’96 Aussois …, 1998 | 20 | 1998 |
| Dependent event types Z Luo, S Soloviev Logic, Language, Information, and Computation: 24th International Workshop …, 2017 | 17 | 2017 |
| A unified categorical approach for attributed graph rewriting M Rebout, L Féraud, S Soloviev Computer Science–Theory and Applications: Third International Computer …, 2008 | 17 | 2008 |
| Homotopy type theory: univalent foundations of mathematics P Aczel, B Ahrens, T Altenkirch, S Awodey, B Barras, A Bauer, Y Bertot, ... The Univalent Foundations Program Institute for Advanced Study, 2013 | 15 | 2013 |
| Coherence and transitivity of subtyping as entailment G Longo, K Milsted, S Soloviev Journal of Logic and Computation 10 (4), 493-526, 2000 | 15 | 2000 |
| Some proof-theoretic and algorithmic aspects of coercive subtyping A Jones, Z Luo, S Soloviev Proc. of the Annual Conf on Types and Proofs (TYPES'96), 1997 | 15 | 1997 |
| A deciding algorithm for linear isomorphism of types with complexity O(nlog 2(n)). A Andreev, S Soloviev Category Theory and Computer Science: 7th International Conference, CTCS'97 …, 1997 | 15 | 1997 |
| Remarks on isomorphisms of simple inductive types D Chemouil, S Soloviev Electronic Notes in Theoretical Computer Science 85 (7), 106-124, 2003 | 13 | 2003 |
| Some algebraic structures in lambda-calculus with inductive types S Soloviev, D Chemouil International Workshop on Types for Proofs and Programs, 338-354, 2003 | 13 | 2003 |
| On natural transformations of distinguished functors and their superpositions in certain closed categories SV Soloviev Journal of Pure and Applied Algebra 47 (2), 181-204, 1987 | 13 | 1987 |
| Coherence in SMCCs and equivalences on derivations in IMLL with unit L Mehats, S Soloviev Annals of Pure and Applied Logic 147 (3), 127-179, 2007 | 12 | 2007 |
| Some proof-theoretic and algorithmic aspects of coercive subtyping. Types for proofs and programs A Jones, Z Luo, S Soloviev Proc. of the Inter. Conf. TYPES 96, 1998 | 11 | 1998 |
