1993 …2024

Research activity per year

If you made any changes in Pure these will be visible here soon.
Filter
Conference contribution

Search results

  • 2018

    Introduction to bidirectional transformations

    Abou-Saleh, F., Cheney, J., Gibbons, J., McKinna, J. & Stevens, P., 28 Mar 2018, Bidirectional Transformations. Stevens, P. & Gibbons, J. (eds.). Springer, p. 1-28 28 p. (Lecture Notes in Computer Science; vol. 9715).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    17 Citations (Scopus)
  • Triangulating context lemmas

    McIaughlin, C., McKinna, J. & Stark, I. D. B., 8 Jan 2018, CPP 2018: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs. Association for Computing Machinery, p. 102-114 13 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    6 Citations (Scopus)
  • 2017

    Type-and-scope safe programs and their proofs

    Allais, G., Chapman, J., McBride, C. & McKinna, J., 16 Jan 2017, CPP 2017: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs. Bertot, Y. & Vafeiadis, V. (eds.). Association for Computing Machinery, p. 195-207 13 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    31 Citations (Scopus)
  • 2015

    Notions of bidirectional computation and entangled state monads

    Abou-Saleh, F., Cheney, J., Gibbons, J., McKinna, J. & Stevens, P., 2015, Mathematics of Program Construction. MPC 2015. Voigtländer, J. & Hinze, R. (eds.). Springer, p. 187-214 28 p. (Lecture Notes in Computer Science; vol. 9129).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    9 Citations (Scopus)
  • The encode-decode method, relationally

    McKinna, J. & Forsberg, F. N., 2015, Abstracts of the 21st International Conference on Types for Proofs and Programs, TYPES 2015. Institute of Cybernetics at Tallinn University of Technology, p. 63-64 2 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 2014

    Certified Complexity (CerCo)

    Amadio, R. M., Ayache, N., Bobot, F., Boender, J. P., Campbell, B., Garnier, I., Madet, A., McKinna, J., Mulligan, D. P., Piccolo, M., Pollack, R., Régis-Gianas, Y., Coen, C. S., Stark, I. & Tranquilli, P., 2014, Foundational and Practical Aspects of Resource Analysis. FOPARA 2013. Lago, U. D. & Peña, R. (eds.). Springer, p. 1-18 18 p. (Lecture Notes in Computer Science; vol. 8552).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    19 Citations (Scopus)
  • 2010

    Proviola: A tool for proof re-animation

    Tankink, C., Geuvers, H., McKinna, J. & Wiedijk, F., 2010, Intelligent Computer Mathematics. CICM 2010. Springer, p. 440-454 15 p. (Lecture Notes in Computer Science; vol. 6167).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    16 Citations (Scopus)
  • 2009

    A logically saturated extension of λ¯μμ~

    Mamane, L. E., Geuvers, H. & McKinna, J., 2009, Intelligent Computer Mathematics. CICM 2009. Springer, p. 405-421 17 p. (Lecture Notes in Computer Science; vol. 5625).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • A machine-checked proof of the average-case complexity of quicksort in coq

    Van Der Weegen, E. & McKinna, J., 2009, Types for Proofs and Programs. TYPES 2008. Springer, p. 256-271 16 p. (Lecture Notes in Computer Science; vol. 5497).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    7 Citations (Scopus)
  • Domain Specific Languages (DSLs) for Network Protocols (Position Paper)

    Bhatti, S., Brady, E., Hammond, K. & McKinna, J., 7 Jul 2009, 2009 29th IEEE International Conference on Distributed Computing Systems Workshops. IEEE, p. 208-213 6 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 2008

    Mechanising a proof of Craig's interpolation theorem for intuitionistic logic in nominal Isabelle

    Chapman, P., McKinna, J. & Urban, C., 2008, Intelligent Computer Mathematics. CICM 2008. Springer, p. 38-52 15 p. (Lecture Notes in Computer Science; vol. 5144).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    3 Citations (Scopus)
  • 2006

    A few constructions on constructors

    McBride, C., Goguen, H. & McKinna, J., 2006, Types for Proofs and Programs. TYPES 2004. Springer, p. 186-200 15 p. (Lecture Notes in Computer Science; vol. 3839).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    13 Citations (Scopus)
  • A Sequent Calculus for Type Theory

    Lengrand, S., Dyckhoff, R. & McKinna, J., 2006, Computer Science Logic. CSL 2006. Springer, p. 441-455 15 p. (Lecture Notes in Computer Science; vol. 4207).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    6 Citations (Scopus)
  • Why dependent types matter

    McKinna, J., Jan 2006, POPL '06: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages. Association for Computing Machinery, p. 1

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    12 Citations (Scopus)
  • 2004

    Functional pearl: i am not a number--i am a free variable

    McBride, C. & McKinna, J., Sept 2004, Haskell '04: Proceedings of the 2004 ACM SIGPLAN workshop on Haskell. Association for Computing Machinery, p. 1-9 9 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 1994

    Checking algorithms for Pure Type Systems

    Benthem Jutting, L. S., McKinna, J. & Pollack, R., 1994, Types for Proofs and Programs. TYPES 1993. Springer, p. 19-61 43 p. (Lecture Notes in Computer Science; vol. 806).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    22 Citations (Scopus)
  • 1993

    Deliverables: A Categorial Approach to Program Development in Type Theory

    McKinna, J. & Burstall, R. M., 1993, Mathematical Foundations of Computer Science 1993. MFCS 1993. Springer, p. 32-67 36 p. (Lecture Notes in Computer Science; vol. 711).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    10 Citations (Scopus)
  • Pure Type Systems Formalized

    McKinna, J. & Pollack, R., 1993, Typed Lambda Calculi and Applications. TLCA 1993. Springer, p. 289-305 17 p. (Lecture Notes in Computer Science; vol. 664).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    64 Citations (Scopus)