References

1. Flow: A Static Type Checker for Javascript. Available at https://flow.org/.
2. Google Closure Compiler. Available at https://developers.google.com/closure/compiler.
3. Hoogle. Available at https://hoogle.haskell.org/.
4. K Framework. Available at http://www.kframework.org/.
5. KJS: A Complete Formal Semantics of JavaScript. Available at https://github.com/kframework/javascript-semantics.
6. Microsoft TypeScript. Available at https://www.typescriptlang.org/.
7. RChain. Available at https://www.rchain.coop/.
8. Steve Awodey (2010): Category Theory, 2nd edition. Oxford University Press, Inc., USA.
9. Steve Awodey (2016): Natural models of homotopy type theory. Mathematical Structures in Computer Science 28(2), pp. 241–286, doi:10.1017/s0960129516000268.
10. H. P. Barendregt (1984): The Lambda Calculus: Its Syntax and Semantics. Elsevier.
11. Gérard Boudol (1997): The -calculus in direct style. In: Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL. ACM Press, doi:10.1145/263699.263726.
12. John Cartmell (1986): Generalised algebraic theories and contextual categories. Annals of Pure and Applied Logic 32, pp. 209–243, doi:10.1016/0168-0072(86)90053-9. Available at https://www.sciencedirect.com/science/article/pii/0168007286900539.
13. Thierry Coquand & Gérard Huet (1988): The calculus of constructions. Information and Computation 76(2-3), pp. 95–120, doi:10.1016/0890-5401(88)90005-3.
14. Roy L. Crole (1994): Categories for Types. Cambridge University Press, doi:10.1017/CBO9781139172707.
15. Robert Harper (2016): Practical Foundations for Programming Languages, 2 edition. Cambridge University Press, doi:10.1017/CBO9781316576892.
16. André Hirschowitz, Tom Hirschowitz & Ambroise Lafont (2020): Modules over monads and operational semantics. ArXiv:2012.06530.
17. B. Jacobs (1998): Categorical Logic and Type Theory. Elsevier, Amsterdam, doi:10.1016/s0049-237x(98)x8028-6.
18. Peter T. Johnstone (2002): Sketches of an Elephant: A Topos Theory Compendium: 2 Volume Set. Oxford University Press UK.
19. J. Lambek & P. J. Scott (1986): Introduction to Higher Order Categorical Logic. Cambridge University Press, USA.
20. F. William Lawvere (1969): Adjointness in Foundations. dialectica 23(3-4), pp. 281–296, doi:10.1111/j.1746-8361.1969.tb01194.x.
21. Saunders MacLane (1971): Categories for the Working Mathematician. Springer New York, doi:10.1007/978-1-4612-9839-7.
22. Saunders MacLane & Ieke Moerdijk (1994): Sheaves in Geometry and Logic. Springer New York, doi:10.1007/978-1-4612-0927-0.
23. Per Martin-Löf (1998): An intuitionistic theory of types. In: Twenty Five Years of Constructive Type Theory. Oxford University Press, doi:10.1093/oso/9780198501275.003.0010.
24. Paul-André Melliès & Noam Zeilberger (2015): Functors are Type Refinement Systems. ACM SIGPLAN Notices 50(1), pp. 3–16, doi:10.1145/2775051.2676970.
25. L. G. Meredith & Matthias Radestock (2005): Namespace Logic: A Logic for a Reflective Higher-Order Calculus. In: Trustworthy Global Computing. Springer Berlin Heidelberg, pp. 353–369, doi:10.1007/11580850_19.
26. L.G. Meredith & Matthias Radestock (2005): A Reflective Higher-order Calculus. Electronic Notes in Theoretical Computer Science 141(5), pp. 49–67, doi:10.1016/j.entcs.2005.05.016.
27. Lucius G Meredith, Mike Stay & Sophia Drossopoulou (2013): Policy as Types. ArXiv:1307.7766.
28. Robin Milner (1993): The Polyadic -Calculus: a Tutorial. In: Logic and Algebra of Specification. Springer Berlin Heidelberg, pp. 203–246, doi:10.1007/978-3-642-58041-3_6.
29. Ieke Moerdijk & Erik Palmgren (2000): Wellfounded trees in categories. Annals of Pure and Applied Logic 104(1-3), pp. 189–218, doi:10.1016/s0168-0072(00)00012-9.
30. Davide Sangiorgi (2000): Communicating and Mobile Systems: the -calculus,. Science of Computer Programming 38(1-3), pp. 151–153, doi:10.1016/s0167-6423(00)00008-3.
31. Dana S. Scott (1980): Relating Theories of the Lambda Calculus. Available at https://www.andrew.cmu.edu/user/awodey/dump/Scott/ScottRelating.pdf.
32. Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau & Théo Winterhalter (2019): Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq. Proc. ACM Program. Lang. 4(POPL), doi:10.1145/3371076.
33. Ross Street (1974): Elementary cosmoi I. In: Gregory M. Kelly: Category Seminar. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 134–180, doi:10.1016/0022-4049(72)90019-9.
34. Andrzej Tarlecki, Rod M. Burstall & Joseph A. Goguen (1991): Some fundamental algebraic tools for the semantics of computation: Part 3. indexed categories. Theoretical Computer Science 91(2), pp. 239 – 264, doi:10.1016/0304-3975(91)90085-G. Available at http://www.sciencedirect.com/science/article/pii/030439759190085G.
35. D. Turi & G. Plotkin: Towards a mathematical operational semantics. In: Proceedings of Twelfth Annual IEEE Symposium on Logic in Computer Science. IEEE Comput. Soc, doi:10.1109/lics.1997.614955.

Comments and questions to: eptcs@eptcs.org

For website issues: webmaster@eptcs.org