Geodesic
Automorphisms of types and their applications
Zapiski Nauchnykh Seminarov POMI, Representation theory, dynamical systems, combinatorial methods. Part XXIX, Tome 468 (2018), pp. 287-308 Cet article a éte moissonné depuis la source Math-Net.Ru

Voir la notice du chapitre de livre

We outline recent results in the theory of type isomorphisms and automorphisms and present several practical applications of said results that can be useful in the contexts of programming and data security. 
@article{ZNSL_2018_468_a19,
     author = {S. Soloviev and J. Malakhovski},
     title = {Automorphisms of types and their applications},
     journal = {Zapiski Nauchnykh Seminarov POMI},
     pages = {287--308},
     year = {2018},
     volume = {468},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/ZNSL_2018_468_a19/}
}
TY  - JOUR
AU  - S. Soloviev
AU  - J. Malakhovski
TI  - Automorphisms of types and their applications
JO  - Zapiski Nauchnykh Seminarov POMI
PY  - 2018
SP  - 287
EP  - 308
VL  - 468
UR  - http://geodesic.mathdoc.fr/item/ZNSL_2018_468_a19/
LA  - en
ID  - ZNSL_2018_468_a19
ER  - 
%0 Journal Article
%A S. Soloviev
%A J. Malakhovski
%T Automorphisms of types and their applications
%J Zapiski Nauchnykh Seminarov POMI
%D 2018
%P 287-308
%V 468
%U http://geodesic.mathdoc.fr/item/ZNSL_2018_468_a19/
%G en
%F ZNSL_2018_468_a19
S. Soloviev; J. Malakhovski. Automorphisms of types and their applications. Zapiski Nauchnykh Seminarov POMI, Representation theory, dynamical systems, combinatorial methods. Part XXIX, Tome 468 (2018), pp. 287-308. http://geodesic.mathdoc.fr/item/ZNSL_2018_468_a19/

[1] L. Babai, “Automorphism Groups, Isomorphism, Reconstruction”, Handbook of Combinatorics, v. 2, Elsevier, 1995, 1447–1541 | MR

[2] H. Barendregt, The Lambda Calculus, Its Syntax and Semantics, revised edition, North-Holland Plc., 1984 | MR | Zbl

[3] D. A. Basin, “Equality of Terms Containing Associative-Commutative Functions and Commutative Binding Operators is Isomorphism Complete”, 10th Int. Conf. on Automated, Lecture Notes in Artificial Intelligence, 449, ed. M. E. Stickel, Springer-Verlag, Kaiserslautern, Germany, 1990, 251–260 | MR

[4] R. Brown, Ph. G. Higgins, R. Sivera, Nonabelian Algebraic Topology, European Math. Soc., 2011 | MR | Zbl

[5] K. Bruce, G. Longo, “Provable isomorphisms and domain equations in models of typed languages”, ACM symposium on theory of computing, STOC 85, 1985, 263–272

[6] M. Dezani-Ciancaglini, “Characterization of normal forms possessing inverse in the $\lambda-\beta-\eta$-calculus”, Theor. Comp. Sci., 2 (1976), 323–337 | DOI | MR | Zbl

[7] R. Di Cosmo, Isomorphisms of types: from lambda-calculus to information retrieval and language design, Birkhauser, 1995 | MR | Zbl

[8] D. Gilles, “A complete proof synthesis method for the cube of type systems”, J. Logic Comp., 3:3 (1993), 287–315 | DOI | MR | Zbl

[9] D. Gilles, “Higher-order unification and matching”, Handbook of automated reasoning, Elsevier Science, 2, no. 16, eds. Alan Robinson, Andrei Voronkov, 2001, 1009–1062 | Zbl

[10] J. (Yossi) Gil, Y. Zibin, “Efficient Algorithms for Isomorphisms of Simple Types”, Math. Struct. Comp. Science, 15:5 (2005), 917–957 | DOI | MR | Zbl

[11] H. Goguen, A Typed Operational Semantics for Type Theory, PhD thesis, University of Edinburgh, 1994 | MR

[12] M. Hall (Jr.), The Theory of Groups, The Macmillan Company, 1959 | MR | Zbl

[13] Chr. Hankin, Lambda Calculi: A Guide for Computer Scientists, Clarendon Press, Oxford, 1994 | MR | Zbl

[14] J. Heather, G. Lowe, S. Schneider, “How to prevent type flaw attacks on security protocols”, J. Comp. Sec., 11:2 (2003), 217–244

[15] J. Hoffstein, J. Pipher, J. H. Silverman, An introduction to mathematical cryptography, Springer, New York, 2008 | MR | Zbl

[16] G. Huet, C. Derek, Oppen, Equations and Rewrite Rules: A Survey, Technical report, Stanford University, 1980

[17] A. Mahalanobis, “The MOR cryptosystem and finite $p$-groups”, Contemp. Math., 633 (2015), 81–95 | DOI | MR | Zbl

[18] A. Martelli, U. Montanari, “An Efficient Unification Algorithm”, ACM Trans. Program. Lang. Syst., 4:2 (1982), 258–282 | DOI | Zbl

[19] F. Lindblad, M. Benke, “A Tool for Automated Theorem Proving in Agda”, Types for Proofs and Programs, TYPES 2004, Lecture Notes in Computer Science, 3839, eds. Paulin-Mohring C., Werner B., Springer, Berlin–Heidelberg, 2006 | MR | Zbl

[20] Z. Luo, Computation and Reasoning, Int. Series Monogr. Comp. Sci., 11, Oxford Science Publications, Clarendon Press, Oxford, UK, 1994 | MR | Zbl

[21] Neil Mitchell et al., Hoogle: Haskell API search engine, https://github.com/ndmitchell/hoogle

[22] M. Rittri, “Using Types as Search Keys in Function Libraries”, Proceedings of the fourth international conference on Functional programming languages and computer architecture, 1989, 174–183

[23] M. Rittri, “Retrieving library functions by unifying types modulo linear isomorphism”, Theor. Inform. Applic., 27 (1993), 71–89 | DOI

[24] C. Runciman, I. Toyn, “Retrieving reusable software components by polymorphic type”, J. Func. Progr., 1:2 (1991), 191–211 | MR | Zbl

[25] S. Soloviev, “On Isomorphism of Dependent Products in a Typed Logical Framework”, Post-proceedings of TYPES 2014, LIPICS, 39, Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2015, 275–288 | MR

[26] S. Soloviev, “Automorphisms of Types in Certain Type Theories and Representation of Finite Groups”, Math. Struct. Comp. Sci., 2018 (to appear)

[27] A. T. White, Graphs, Groups and Surfaces, North-Holland, Amsterdam, 1984 | MR | Zbl