A Type-Theoretical Study of Nontermination

Agda code

• Agda code for Chapters 2, 3 and 4.
  Part of the code accompanies the following paper and its journal version (currently under review):
  
  Chapman, J., Uustalu, T., Veltri, N.: Quotienting the delay monad by weak bisimilarity.
  In: Leucker, M., Rueda, C., Valencia, F. D. (eds.) ICTAC 2015, LNCS, vol. 9399, pp. 110-125, Springer (2015)
  
  
• Agda code for the Appendix.
  The code accompanies the following paper:
  
  Chapman, J., Uustalu, T., Veltri, N.: Formalizing restriction categories.
  J. Formalized Reasoning, 10(1), 1-36 (2017)