@article(ALS21,
 author       = {G. Ambal and S. Lenglet and A. Schmitt},
 year         = {2021},
 title        = {HO{$\pi$} in Coq},
 journal      = {Journal of Automated Reasoning},
 volume       = {65},
 pages        = {75--124},
 doi          = {10.1007/s10817-020-09553-0},
)
@book(Bar84,
 author       = {H. P. Barendregt},
 year         = {1984},
 title        = {The Lambda Calculus---Its Syntax and Semantics},
 publisher    = {North-Holland},
)
@inproceedings(BBLPPS17,
 author       = {M. Biernacka and D. Biernacki and S. Lenglet and P. Polesiuk and D. Pous and A. Schmitt},
 year         = {2017},
 title        = {Fully Abstract Encodings of $\lambda$-Calculus in HOcore through Abstract Machines},
 booktitle    = {Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017)},
 pages        = {1--12},
 doi          = {10.1109/LICS.2017.8005118},
)
@article(Bru72,
 author       = {N.G. De Bruijn},
 year         = {1972},
 title        = {Lambda Calculus Notation with Nameless Dummies: A Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem},
 journal      = {Indagationes Mathematicae},
 volume       = {34},
 pages        = {381--392},
 doi          = {10.1016/1385-7258(72)90034-0},
)
@techreport(BGH04,
 author       = {M. Bundgaard and J. C. Godskesen and T. Hildebrandt},
 year         = {2004},
 title        = {Bisimulation Congruences for Homer ? A Calculus of Higher Order Mobile Embedded Resources},
 type         = {Technical Report},
 institution  = {IT University of Copenhagen},
)
@inproceedings(BGHH09,
 author       = {M. Bundgaard and J. Chr. Godskesen and B. Haagensen and H. H\"{u}ttel},
 year         = {2009},
 title        = {Decidable Fragments of a Higher Order Calculus with Locations},
 booktitle    = {Proceedings of the 15th International Workshop on Expressiveness in Concurrency (EXPRESS 2008)},
 volume       = {Electronic Notes in Theoretical Computer Science 242(1)},
 pages        = {113--138},
 doi          = {10.1016/j.entcs.2009.06.016},
)
@article(BGZ09,
 author       = {N. Busi and M. Gabbrielli and G. Zavattaro},
 year         = {2009},
 title        = {On the Expressive Power of Recursion, Replication and Iteration in Process Calculi},
 journal      = {Mathematical Structures in Computer Science},
 volume       = {19},
 pages        = {1191--1222},
 doi          = {10.1017/S096012950999017X},
)
@inproceedings(CT01,
 author       = {W. Charatonik and J.-M. Talbot},
 year         = {2001},
 title        = {The Decidability of Model Checking Mobile Ambients},
 booktitle    = {In Proceedings of the 15th International Workshop on Computer Science Logic (CSL 2001)},
 series       = {Lecture Notes in Computer Science},
 volume       = {2142},
 pages        = {339--354},
 doi          = {10.1007/3-540-44802-0\_24},
)
@article(CHM94,
 author       = {S. Christensen and Y. Hirshfeld and F. Moller},
 year         = {1994},
 title        = {Decidable Subsets of CCS},
 journal      = {The Computer Journal},
 volume       = {37},
 pages        = {233--242},
 doi          = {10.1093/comjnl/37.4.233},
)
@inproceedings(GPZ09,
 author       = {C. Di Giusto and J. A. P\'{e}rez and G. Zavattaro},
 year         = {2009},
 title        = {On the Expressiveness of Forwarding in Higher-Order Communication},
 booktitle    = {In Proceedings of the 6th International Colloquium on Theoretical Aspects of Computing (ICTAC 2009)},
 series       = {Lecture Notes in Computer Science},
 volume       = {5684},
 pages        = {155--169},
 doi          = {10.1007/978-3-642-03466-4\_10},
)
@article(Jan95,
 author       = {Jan\v{c}ar, P.},
 year         = {1995},
 title        = {Undecidability of Bisimilarity for Petri Nets and Some Related Problems},
 journal      = {Theoretical Computer Science},
 volume       = {148},
 pages        = {281--301},
 doi          = {10.1016/0304-3975(95)00037-W},
)
@article(KH12,
 author       = {V. Koutavas and M. Hennessy},
 year         = {2012},
 title        = {First-order Reasoning for Higher-order Concurrency},
 journal      = {Computer Languages, Systems and Structures},
 volume       = {38},
 pages        = {242--277},
 doi          = {10.1016/j.cl.2012.04.003},
)
@article(KJ06,
 author       = {Ku\v{c}era, A. and Jan\v{c}ar, P.},
 year         = {2006},
 title        = {Equivalence-checking on Infinite-state Systems: Techniques and Results},
 journal      = {Theory and Practice of Logic Programming},
 volume       = {6},
 pages        = {227--264},
 doi          = {10.1017/S1471068406002651},
)
@inproceedings(LPSS10,
 author       = {I. Lanese and J. A. P\'{e}rez and D. Sangiorgi and A. Schmitt},
 year         = {2010},
 title        = {On the Expressiveness of Polyadic and Synchronous Communication in Higher-order Process Calculi},
 booktitle    = {In Proceedings of 37th International Colloquium on Automata, Languages and Programming (ICALP 2010)},
 series       = {Lecture Notes in Computer Science},
 volume       = {6199},
 pages        = {442--453},
 doi          = {10.1007/978-3-642-14162-1\_37},
)
@article(LPSS10a,
 author       = {I. Lanese and J. A. P\'{e}rez and D. Sangiorgi and A. Schmitt},
 year         = {2011},
 title        = {On the Expressiveness and Decidability of Higher-Order Process Calculi},
 journal      = {Information and Computation},
 volume       = {209(2)},
 pages        = {198--226},
 doi          = {10.1016/j.ic.2010.10.001},
)
@book(Mil89,
 author       = {R. Milner},
 year         = {1989},
 title        = {Communication and Concurrency},
 publisher    = {Prentice Hall},
)
@article(MM93,
 author       = {R. Milner and F. Moller},
 year         = {1993},
 title        = {Unique Decomposition of Processes},
 journal      = {Theoretical Computer Science},
 volume       = {107(2)},
 pages        = {357--363},
 doi          = {10.1016/0304-3975(93)90176-t},
)
@phdthesis(Per10,
 author       = {J.A. P\'{e}rez},
 year         = {2010},
 title        = {Higher-Order Concurrency: Expressiveness and Decidability Results},
 type         = {Phd thesis},
 school       = {University of Bologna, Italy},
)
@phdthesis(San92,
 author       = {D. Sangiorgi},
 year         = {1992},
 title        = {Expressing Mobility in Process Algebras: First-order and Higher-order Paradigms},
 type         = {Phd thesis},
 school       = {University of Edinburgh},
)
@article(San96,
 author       = {D. Sangiorgi},
 year         = {1996},
 title        = {Pi-calculus, Internal Mobility and Agent-Passing Calculi},
 journal      = {Theoretical Computer Science},
 volume       = {167(2)},
 doi          = {10.1016/0304-3975(96)00075-8},
 note         = {Extracts of parts of the material contained in this paper can be found in the Proceedings of TAPSOFT'95 and ICALP'95},
)
@book(SW01a,
 author       = {D. Sangiorgi and D. Walker},
 year         = {2001},
 title        = {The Pi-calculus: a Theory of Mobile Processes},
 publisher    = {Cambridge Universtity Press},
)
@inproceedings(SS05,
 author       = {A. Schmitt and J. B. Stefani},
 year         = {2004},
 title        = {The Kell Calculus: a Family of Higher-order Distributed Process Calculi},
 booktitle    = {In IST/FET International Workshop on Global Computing},
 series       = {Lecture Notes in Computer Science},
 volume       = {3267},
 pages        = {146--178},
 doi          = {10.1007/978-3-540-31794-4\_9},
)
@inproceedings(Sch01,
 author       = {P. Schnoebelen},
 year         = {2001},
 title        = {Bisimulation and Other Undecidable Equivalences for Lossy Channel Systems},
 booktitle    = {In Proceedings of 4th International Symposium on Theoretical Aspects of Computer Software (TACS?01)},
 series       = {Lecture Notes in Computer Science},
 volume       = {2215},
 pages        = {385--399},
 doi          = {10.1007/3-540-45500-0\_19},
)
@article(Tho93,
 author       = {B. Thomsen},
 year         = {1993},
 title        = {Plain {CHOCS}, a Second Generation Calculus for Higher-Order Processes},
 journal      = {Acta Informatica},
 volume       = {30(1)},
 pages        = {1--59},
 doi          = {10.1007/BF01200262},
)
@article(Xu20,
 author       = {Xian Xu},
 year         = {2020},
 title        = {Parameterizing Higher-order Processes on Names and Processes},
 journal      = {RAIRO - Theoretical Informatics and Applications},
 volume       = {53},
 number       = {3-4},
 pages        = {153--206},
 doi          = {10.1051/ita/2019005},
)
@(XZ21L,
 author       = {Xian Xu and Wenbo Zhang},
 year         = {2021},
 title        = {On Decidability of the Bisimilarity on Higher-order Processes with Parameterization (long version)},
 url          = {http://basics.sjtu.edu.cn/~xuxian/main_HO_DEC_with_appendix.pdf},
)
@article(YXL17,
 author       = {Qiang Yin and Xian Xu and Huan Long},
 year         = {2017},
 title        = {On Parameterization of Higher-order Processes},
 journal      = {International Journal of Computer Mathematics},
 volume       = {94(7)},
 pages        = {1451--1478},
 doi          = {10.1080/00207160.2016.1210793},
)