skip to content
Home

Department of Computer Science and Technology

Machine Learning and Artificial Intelligence Subscribe to RSS - Machine Learning and Artificial Intelligence

Read more at: Andrew Rice

Andrew Rice

I am Professor of Computer Science in the University of Cambridge Department of Computer Science and Technology and the Hassabis Fellow in Computer Science and Director of Studies in Computer Science at Queens' College.

My current research activity focuses on programming and software engineering:

Journal articles

  • Contrastin, M., Charman, RH., Danish, M., Orchard, B., Orchard, D., Rice, A. and Xu, J., 2025. fortran-src: Fortran static analysis infrastructure Journal of Open Source Software, v. 10
    Doi: http://doi.org/10.21105/joss.07571
    •
  • Orchard, D., Contrastin, M., Danish, M. and Rice, AC., 2019. Verifying spatial properties of array computations. PACMPL, v. 1
    •
  • Rice, A., Aftandilian, E., Jaspan, C., Johnston, E., Pradel, M. and Arroyo-Paredes, Y., 2017. Detecting Argument Selection Defects PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, v. 1
    Doi: 10.1145/3133928
    •
  • Orchard, D., Contrastin, M., Danish, M. and Rice, A., 2017. Verifying spatial properties of array computations Proceedings of the ACM on Programming Languages, v. 1
    Doi: 10.1145/3133899
    •
  • Contrastin, M., Rice, A., Danish, M. and Orchard, D., 2016. Units-of-Measure Correctness in Fortran Programs Computing in Science and Engineering, v. 18
    Doi: 10.1109/MCSE.2016.17
    •
  • Contrastin, M., Danish, M., Orchard, D. and Rice, A., 2016. Lightning talk: Supporting software sustainability with lightweight specifications Ceur Workshop Proceedings, v. 1686
    •
  • Cummins, S., Beresford, AR. and Rice, A., 2016. Investigating Engagement with In-Video Quiz Questions in a Programming Course IEEE Transactions on Learning Technologies, v. 9
    Doi: 10.1109/TLT.2015.2444374
    •
  • Orchard, D., Rice, A. and Oshmyan, O., 2015. Evolving Fortran types with inferred units-of-measure Journal of Computational Science, v. 9
    Doi: 10.1016/j.jocs.2015.04.018
    •
  • Wagner, DT., Rice, A. and Beresford, AR., 2014. Device analyzer: Largescale mobile data collection Performance Evaluation Review, v. 41
    Doi: 10.1145/2627534.2627553
    •
  • Linnap, M. and Rice, A., 2014. Managed Participatory Sensing with YouSense JOURNAL OF URBAN TECHNOLOGY, v. 21
    Doi: 10.1080/10630732.2014.888216
    •
  • Bazilian, M., Rice, A., Rotich, J., Howells, M., DeCarolis, J., Macmillan, S., Brooks, C., Bauer, F. and Liebreich, M., 2012. Open source software and crowdsourcing for energy analysis Energy Policy,
    •
  • Bazilian, M., Rice, A., Rotich, J., Howells, M., DeCarolis, J., Macmillan, S., Brooks, C., Bauer, F. and Liebreich, M., 2012. Open source software and crowdsourcing for energy analysis Energy Policy, v. 49
    Doi: 10.1016/j.enpol.2012.06.032
    •
  • Akoush, S., Sohan, R., Roman, B., Rice, A. and Hopper, A., 2011. Activity based sector synchronisation: Efficient transfer of disk-state for WAN live migration IEEE International Workshop on Modeling Analysis and Simulation of Computer and Telecommunication Systems Proceedings,
    Doi: 10.1109/MASCOTS.2011.20
    •
  • Rice, AC. and Hay, S., 2010. Measuring mobile phone energy consumption for 802.11 wireless networking. Pervasive Mob. Comput., v. 6
    Doi: 10.1016/j.pmcj.2010.07.005
    •
  • Hylick, A., Rice, AC., Jones, B. and Sohan, R., 2007. Hard drive power consumption uncovered. SIGMETRICS Perform. Evaluation Rev., v. 35
    Doi: 10.1145/1328690.1328714
    •

    Theses / dissertations

  • Fekry, A., 2021 (No publication date). Optimizing Data-Intensive Computing with Efficient Configuration Tuning
  • Timmons, N., 2021 (No publication date). Software-based approximate computing for mathematical functions
    Doi: 10.17863/CAM.78442
    •

    Conference proceedings

  • Zaidi, A., Caines, A., Moore, R., Buttery, P. and Rice, A., 2020. Adaptive Forgetting Curves for Spaced Repetition Language Learning Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, v. 12164 LNAI
    Doi: 10.1007/978-3-030-52240-7_65
    •
  • Fekry, A., Carata, L., Pasquier, T., Rice, A. and Hopper, A., 2020. To Tune or Not to Tune?: In Search of Optimal Configurations for Data Analytics Proceedings of the ACM SIGKDD International Conference on Knowledge Discovery and Data Mining,
    Doi: 10.1145/3394486.3403299
    •
  • Tarlow, D., Moitra, S., Rice, A., Chen, Z., Manzagol, PA., Sutton, C. and Aftandilian, E., 2020. Learning to Fix Build Errors with Graph2Diff Neural Networks Proceedings - 2020 IEEE/ACM 42nd International Conference on Software Engineering Workshops, ICSEW 2020,
    Doi: 10.1145/3387940.3392181
    •
  • Fekry, A., Carata, L., Pasquier, T. and Rice, A., 2020. Accelerating the Configuration Tuning of Big Data Analytics with Similarity-aware Multitask Bayesian Optimization Proceedings 2020 IEEE International Conference on Big Data Big Data 2020,
    Doi: 10.1109/BigData50022.2020.9378085
    •
  • Mesbah, A., Rice, A., Aftandilian, E., Johnston, E. and Glorioso, N., 2019 (Accepted for publication). DeepDelta: Learning to Repair Compilation Errors
    Doi: 10.17863/CAM.42065
    •
  • Moore, R., Caines, A., Elliott, M., Zaidi, A., Rice, A. and Buttery, P., 2019. Skills embeddings: A neural approach to multicomponent representations of students and tasks Edm 2019 Proceedings of the 12th International Conference on Educational Data Mining,
    •
  • Zaidi, AH., Caines, A., Davis, C., Moore, R., Buttery, P. and Rice, A., 2019. Accurate modelling of language learning tasks and students using representations of grammatical proficiency Edm 2019 Proceedings of the 12th International Conference on Educational Data Mining,
    •
  • Fekry, A., Carata, L., Pasquier, T., Rice, A. and Hopper, A., 2019. Towards seamless configuration tuning of big data analytics Proceedings International Conference on Distributed Computing Systems, v. 2019-July
    Doi: 10.1109/ICDCS.2019.00189
    •
  • Rice, AC. and Licker, N., 2019. Detecting Incorrect Build Rules
    Doi: 10.17863/CAM.35755
    •
  • Danish, M., Allamanis, M., Brockschmidt, M., Rice, A. and Orchard, D., 2019. Learning units-of-measure from scientific code Proceedings 2019 IEEE ACM 14th International Workshop on Software Engineering for Science Se4science 2019,
    Doi: 10.1109/SE4Science.2019.00013
    •
  • Moore, R., Caines, A., Rice, A. and Buttery, P., 2019. Behavioural cloning of teachers for automatic homework selection Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), v. 11625 LNAI
    Doi: 10.1007/978-3-030-23204-7_28
    •
  • Contrastin, M., Rice, AC. and Orchard, D., 2018 (Accepted for publication). Automatic reordering for dataflow safety of Datalog Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming,
    Doi: 10.1145/3236950.3236954
    •
  • Hintze, D. and Rice, A., 2016. Picky: Efficient and Reproducible Sharing of Large Datasets using Merkle-Trees 2016 IEEE 24TH INTERNATIONAL SYMPOSIUM ON MODELING, ANALYSIS AND SIMULATION OF COMPUTER AND TELECOMMUNICATION SYSTEMS (MASCOTS),
    Doi: 10.1109/MASCOTS.2016.25
    •
  • Cummins, S., Stead, A., Jardine-Wright, L., Davies, I., Beresford, AR. and Rice, A., 2016. Investigating the use of hints in online problem solving L@S 2016 - Proceedings of the 3rd 2016 ACM Conference on Learning at Scale,
    Doi: 10.1145/2876034.2893379
    •
  • Cummins, S., Beresford, AR., Davies, I. and Rice, A., 2016. Supporting Authentication and Scalable Data Sharing in Online Education L@S 2016 - Proceedings of the 3rd 2016 ACM Conference on Learning at Scale,
    Doi: 10.1145/2876034.2893376
    •
  • Patrick, M., Elderfield, J., Stutt, ROJH., Rice, A. and Gilligan, CA., 2016. Software testing in a scientific research group Proceedings of the ACM Symposium on Applied Computing, v. 04-08-April-2016
    Doi: 10.1145/2851613.2851783
    •
  • Gechter, F., Beresford, AR. and Rice, A., 2016. Reconstruction of battery level curves based on user data collected from a smartphone Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, v. 9883 LNAI
    Doi: 10.1007/978-3-319-44748-3_28
    •
  • Faragher, R. and Rice, A., 2015 (Accepted for publication). SwiftScan: Efficient Wi-Fi scanning for background location-based services
    Doi: 10.17863/CAM.43449
    •
  • Snee, J., Carata, L., Chick, ORA., Sohan, R., Faragher, RM., Rice, A. and Hopper, A., 2015. Soroban: Attributing latency in virtualized environments 7th USENIX Workshop on Hot Topics in Cloud Computing, HotCloud 2015,
    •
  • Snee, J., Carata, L., Chick, ORA., Sohan, R., Faragher, RM., Rice, A. and Hopper, A., 2015. Soroban: Attributing latency in virtualized environments 7th Usenix Workshop on Hot Topics in Cloud Computing Hotcloud 2015,
    •
  • Cummins, S., Davies, I., Rice, A. and Beresford, AR., 2015. Equality: A tool for free-form equation editing Proceedings IEEE 15th International Conference on Advanced Learning Technologies Advanced Technologies for Supporting Open Access to Formal and Informal Learning Icalt 2015,
    Doi: 10.1109/ICALT.2015.34
    •
  • Thomas, DR., Beresford, AR. and Rice, A., 2015. Security metrics for the Android ecosystem SPSM 2015 - Proceedings of the 5th Annual ACM CCS Workshop on Security and Privacy in Smartphones and Mobile Devices, co-located with: CCS 2015,
    Doi: 10.1145/2808117.2808118
    •
  • Snee, J., Carata, L., Chick, ORA., Sohan, R., Faragher, RM., Rice, A. and Hopper, A., 2015. Soroban: Attributing latency in virtualized environments 7th USENIX Workshop on Hot Topics in Cloud Computing, HotCloud 2015,
    •
  • Wagner, DT., Thomas, DR., Beresford, AR. and Rice, A., 2015. Device analyzer: A privacy-aware platform to support research on the android ecosystem Proceedings of the 8th ACM Conference on Security and Privacy in Wireless and Mobile Networks Wisec 2015,
    Doi: 10.1145/2766498.2774992
    •
  • Rice, A. and Beresford, AR., 2014. The device analyzer competition Ubicomp 2014 Adjunct Proceedings of the 2014 ACM International Joint Conference on Pervasive and Ubiquitous Computing,
    Doi: 10.1145/2638728.2641696
    •
  • Wagner, DT., Rice, A. and Beresford, AR., 2014. Device analyzer: Understanding smartphone usage Lecture Notes of the Institute for Computer Sciences Social Informatics and Telecommunications Engineering Lnicst, v. 131
    Doi: 10.1007/978-3-319-11569-6_16
    •
  • Ding, N., Wagner, D., Chen, X., Pathak, A., Hu, YC. and Rice, AC., 2013 (Accepted for publication). Characterizing and modeling the impact of wireless signal strength on smartphone battery drain Proceedings of the ACM SIGMETRICS/international conference on Measurement and modeling of computer systems,
    Doi: 10.1145/2465529.2466586
    •
  • Carata, L., Sohan, R., Rice, A. and Hopper, A., 2013. IPAPI: Designing an improved provenance API 5th Workshop on the Theory and Practice of Provenance Tapp 2013,
    •
  • Ding, N., Wagner, D., Chen, X., Hu, YC. and Rice, A., 2013. Characterizing and modeling the impact of wireless signal strength on smartphone battery drain Performance Evaluation Review, v. 41
    Doi: 10.1145/2494232.2466586
    •
  • Rice, A. and Turner, SJ., 2011. Message from the MASCOTS 2011 program chairs IEEE International Workshop on Modeling Analysis and Simulation of Computer and Telecommunication Systems Proceedings,
    Doi: 10.1109/MASCOTS.2011.5
    •
  • Beresford, AR., Rice, A., Skehin, N. and Sohan, R., 2011. MockDroid: trading privacy for application functionality on smartphones In the Proceedings of the 11th Workshop on Mobile Computing Systems and Applications (HotMobile),
    •
  • Akoush, S., Sohan, R., Rice, A., Moore, AW. and Hopper, A., 2011. Free lunch: Exploiting renewable energy for computing 13th Workshop on Hot Topics in Operating Systems Hotos 2011,
    •
  • Sohan, RS., Akoush, SA., Rice, AC., Moore, AW. and Hopper, A., 2011. Free Lunch: Exploiting Renewable Energy For Computing
  • Rice, AC. and Hay, S., 2010. Decomposing power measurements for mobile devices. PerCom,
    Doi: 10.1109/PERCOM.2010.5466991
    •
  • Rice, AC. and Woodman, OJ., 2010. Crowd-sourcing world models with OpenRoomMap. PerCom Workshops,
    Doi: 10.1109/PERCOMW.2010.5470536
    •
  • Rice, A., Hay, S. and Ryder-Cook, D., 2010. A limited-data model of building energy consumption Proceedings of the 2nd ACM Workshop on Embedded Sensing Systems for Energy-Efficiency in Building - BuildSys ’10,
    Doi: 10.1145/1878431.1878447
    •
  • Vallina-Rodriguez, N., Hui, P., Crowcroft, J. and Rice, AC., 2010. Exhausting battery statistics: understanding the energy demands on mobile handsets. MobiHeld,
    •
  • Akoush, S., Sohan, R., Rice, A., Moore, AW. and Hopper, A., 2010. Predicting the performance of virtual machine migration Proceedings 18th Annual IEEE ACM International Symposium on Modeling Analysis and Simulation of Computer and Telecommunication Systems Mascots 2010,
    Doi: 10.1109/MASCOTS.2010.13
    •
  • Sohan, R., Rice, A., Moore, AW. and Mansley, K., 2010. Characterizing 10 Gbps network interface energy consumption Proceedings Conference on Local Computer Networks LCN,
    Doi: 10.1109/LCN.2010.5735719
    •
  • Hay, S. and Rice, A., 2009. The case for apportionment Proceedings of the First ACM Workshop on Embedded Sensing Systems for Energy-Efficiency in Buildings - BuildSys ’09,
    Doi: 10.1145/1810279.1810283
    •
  • Hylick, A., Sohan, R., Rice, AC. and Jones, B., 2008. An Analysis of Hard Drive Energy Consumption. MASCOTS,
    •
  • Hopper, A. and Rice, A., 2008. Computing for the future of the planet. Philos Trans A Math Phys Eng Sci, v. 366
    Doi: 10.1098/rsta.2008.0124
    •
  • Rice, AC., Beresford, AR. and Harle, RK., 2006. Cantag: An open source software toolkit for designing and deploying marker-based vision systems PERCOM 2006: FOURTH ANNUAL IEEE INTERNATIONAL CONFERENCE ON PERVASIVE COMPUTING AND COMMUNICATIONS, PROCEEDINGS,
    •
  • Rice, AC. and Beresford, AR., 2006. Dependability and accountability for context-aware middleware systems FOURTH ANNUAL IEEE INTERNATIONAL CONFERENCE ON PERVASIVE COMPUTING AND COMMUNICATIONS WORKSHOPS, PROCEEDINGS,
    •
  • Rice, AC., Harle, RK. and Beresford, AR., 2006. Analysing fundamental properties of marker-based vision system designs. Pervasive Mob. Comput., v. 2
    Doi: 10.1016/j.pmcj.2006.07.006
    •
  • Rice, AC. and Harle, RK., 2005. Evaluating lateration-based positioning algorithms for fine-grained tracking. DIALM-POMC,
    •
  • Rice, AC., Cain, CB. and Fawcett, JK., 2005. Dependable coding of fiducial tags UBIQUITOUS COMPUTING SYSTEMS, v. 3598
    •

    Datasets

  • Rice, AC. and Licker, N., 2019. Detecting Incorrect Build Rules - Artifact
    Doi: 10.17863/CAM.35270
    •
  • Orchard, D., Contrastin, M., Danish, M. and Rice, AC., 2017. Research data supporting Verifying Spatial Properties of Array Computations
    Doi: 10.17863/CAM.12627
    •
  • Thomas, DR., Wagner, DT., Beresford, AR. and Rice, A., 2015 (No publication date). Supporting data for: "Security metrics for the Android ecosystem"

    • Book chapters

  • Audzevich, Y., Moore, AW., Rice, AC., Sohan, R., Timotheou, S., Crowcroft, J., Akoush, S., Hopper, A., Wonfor, A., Wang, H., Penty, RV., White, IH., Dong, X., El-Gorashi, TEH. and Elmirghani, JMH., 2012. Intelligent Energy-Aware Networks.
    • Journal articles

    2025

  • Contrastin, M., Charman, RH., Danish, M., Orchard, B., Orchard, D., Rice, A. and Xu, J., 2025. fortran-src: Fortran static analysis infrastructure Journal of Open Source Software, v. 10
    Doi: http://doi.org/10.21105/joss.07571
    •

    2019

  • Orchard, D., Contrastin, M., Danish, M. and Rice, AC., 2019. Verifying spatial properties of array computations. PACMPL, v. 1
    •

    2017

  • Rice, A., Aftandilian, E., Jaspan, C., Johnston, E., Pradel, M. and Arroyo-Paredes, Y., 2017. Detecting Argument Selection Defects PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, v. 1
    Doi: 10.1145/3133928
    •
  • Orchard, D., Contrastin, M., Danish, M. and Rice, A., 2017. Verifying spatial properties of array computations Proceedings of the ACM on Programming Languages, v. 1
    Doi: 10.1145/3133899
    •

    2016

  • Contrastin, M., Rice, A., Danish, M. and Orchard, D., 2016. Units-of-Measure Correctness in Fortran Programs Computing in Science and Engineering, v. 18
    Doi: 10.1109/MCSE.2016.17
    •
  • Contrastin, M., Danish, M., Orchard, D. and Rice, A., 2016. Lightning talk: Supporting software sustainability with lightweight specifications Ceur Workshop Proceedings, v. 1686
    •
  • Cummins, S., Beresford, AR. and Rice, A., 2016. Investigating Engagement with In-Video Quiz Questions in a Programming Course IEEE Transactions on Learning Technologies, v. 9
    Doi: 10.1109/TLT.2015.2444374
    •

    2015

  • Orchard, D., Rice, A. and Oshmyan, O., 2015. Evolving Fortran types with inferred units-of-measure Journal of Computational Science, v. 9
    Doi: 10.1016/j.jocs.2015.04.018
    •

    2014

  • Wagner, DT., Rice, A. and Beresford, AR., 2014. Device analyzer: Largescale mobile data collection Performance Evaluation Review, v. 41
    Doi: 10.1145/2627534.2627553
    •
  • Linnap, M. and Rice, A., 2014. Managed Participatory Sensing with YouSense JOURNAL OF URBAN TECHNOLOGY, v. 21
    Doi: 10.1080/10630732.2014.888216
    •

    2012

  • Bazilian, M., Rice, A., Rotich, J., Howells, M., DeCarolis, J., Macmillan, S., Brooks, C., Bauer, F. and Liebreich, M., 2012. Open source software and crowdsourcing for energy analysis Energy Policy,
    •
  • Bazilian, M., Rice, A., Rotich, J., Howells, M., DeCarolis, J., Macmillan, S., Brooks, C., Bauer, F. and Liebreich, M., 2012. Open source software and crowdsourcing for energy analysis Energy Policy, v. 49
    Doi: 10.1016/j.enpol.2012.06.032
    •

    2011

  • Akoush, S., Sohan, R., Roman, B., Rice, A. and Hopper, A., 2011. Activity based sector synchronisation: Efficient transfer of disk-state for WAN live migration IEEE International Workshop on Modeling Analysis and Simulation of Computer and Telecommunication Systems Proceedings,
    Doi: 10.1109/MASCOTS.2011.20
    •

    2010

  • Rice, AC. and Hay, S., 2010. Measuring mobile phone energy consumption for 802.11 wireless networking. Pervasive Mob. Comput., v. 6
    Doi: 10.1016/j.pmcj.2010.07.005
    •

    2007

  • Hylick, A., Rice, AC., Jones, B. and Sohan, R., 2007. Hard drive power consumption uncovered. SIGMETRICS Perform. Evaluation Rev., v. 35
    Doi: 10.1145/1328690.1328714
    •
    Theses / dissertations

    2021 (No publication date)

  • Fekry, A., 2021 (No publication date). Optimizing Data-Intensive Computing with Efficient Configuration Tuning
  • Timmons, N., 2021 (No publication date). Software-based approximate computing for mathematical functions
    Doi: 10.17863/CAM.78442
    •
    Conference proceedings

    2020

  • Zaidi, A., Caines, A., Moore, R., Buttery, P. and Rice, A., 2020. Adaptive Forgetting Curves for Spaced Repetition Language Learning Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, v. 12164 LNAI
    Doi: 10.1007/978-3-030-52240-7_65
    •
  • Fekry, A., Carata, L., Pasquier, T., Rice, A. and Hopper, A., 2020. To Tune or Not to Tune?: In Search of Optimal Configurations for Data Analytics Proceedings of the ACM SIGKDD International Conference on Knowledge Discovery and Data Mining,
    Doi: 10.1145/3394486.3403299
    •
  • Tarlow, D., Moitra, S., Rice, A., Chen, Z., Manzagol, PA., Sutton, C. and Aftandilian, E., 2020. Learning to Fix Build Errors with Graph2Diff Neural Networks Proceedings - 2020 IEEE/ACM 42nd International Conference on Software Engineering Workshops, ICSEW 2020,
    Doi: 10.1145/3387940.3392181
    •
  • Fekry, A., Carata, L., Pasquier, T. and Rice, A., 2020. Accelerating the Configuration Tuning of Big Data Analytics with Similarity-aware Multitask Bayesian Optimization Proceedings 2020 IEEE International Conference on Big Data Big Data 2020,
    Doi: 10.1109/BigData50022.2020.9378085
    •

    2019 (Accepted for publication)

  • Mesbah, A., Rice, A., Aftandilian, E., Johnston, E. and Glorioso, N., 2019 (Accepted for publication). DeepDelta: Learning to Repair Compilation Errors
    Doi: 10.17863/CAM.42065
    •

    2019

  • Moore, R., Caines, A., Elliott, M., Zaidi, A., Rice, A. and Buttery, P., 2019. Skills embeddings: A neural approach to multicomponent representations of students and tasks Edm 2019 Proceedings of the 12th International Conference on Educational Data Mining,
    •
  • Zaidi, AH., Caines, A., Davis, C., Moore, R., Buttery, P. and Rice, A., 2019. Accurate modelling of language learning tasks and students using representations of grammatical proficiency Edm 2019 Proceedings of the 12th International Conference on Educational Data Mining,
    •
  • Fekry, A., Carata, L., Pasquier, T., Rice, A. and Hopper, A., 2019. Towards seamless configuration tuning of big data analytics Proceedings International Conference on Distributed Computing Systems, v. 2019-July
    Doi: 10.1109/ICDCS.2019.00189
    •
  • Rice, AC. and Licker, N., 2019. Detecting Incorrect Build Rules
    Doi: 10.17863/CAM.35755
    •
  • Danish, M., Allamanis, M., Brockschmidt, M., Rice, A. and Orchard, D., 2019. Learning units-of-measure from scientific code Proceedings 2019 IEEE ACM 14th International Workshop on Software Engineering for Science Se4science 2019,
    Doi: 10.1109/SE4Science.2019.00013
    •
  • Moore, R., Caines, A., Rice, A. and Buttery, P., 2019. Behavioural cloning of teachers for automatic homework selection Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), v. 11625 LNAI
    Doi: 10.1007/978-3-030-23204-7_28
    •

    2018 (Accepted for publication)

  • Contrastin, M., Rice, AC. and Orchard, D., 2018 (Accepted for publication). Automatic reordering for dataflow safety of Datalog Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming,
    Doi: 10.1145/3236950.3236954
    •

    2016

  • Hintze, D. and Rice, A., 2016. Picky: Efficient and Reproducible Sharing of Large Datasets using Merkle-Trees 2016 IEEE 24TH INTERNATIONAL SYMPOSIUM ON MODELING, ANALYSIS AND SIMULATION OF COMPUTER AND TELECOMMUNICATION SYSTEMS (MASCOTS),
    Doi: 10.1109/MASCOTS.2016.25
    •
  • Cummins, S., Stead, A., Jardine-Wright, L., Davies, I., Beresford, AR. and Rice, A., 2016. Investigating the use of hints in online problem solving L@S 2016 - Proceedings of the 3rd 2016 ACM Conference on Learning at Scale,
    Doi: 10.1145/2876034.2893379
    •
  • Cummins, S., Beresford, AR., Davies, I. and Rice, A., 2016. Supporting Authentication and Scalable Data Sharing in Online Education L@S 2016 - Proceedings of the 3rd 2016 ACM Conference on Learning at Scale,
    Doi: 10.1145/2876034.2893376
    •
  • Patrick, M., Elderfield, J., Stutt, ROJH., Rice, A. and Gilligan, CA., 2016. Software testing in a scientific research group Proceedings of the ACM Symposium on Applied Computing, v. 04-08-April-2016
    Doi: 10.1145/2851613.2851783
    •
  • Gechter, F., Beresford, AR. and Rice, A., 2016. Reconstruction of battery level curves based on user data collected from a smartphone Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, v. 9883 LNAI
    Doi: 10.1007/978-3-319-44748-3_28
    •

    2015 (Accepted for publication)

  • Faragher, R. and Rice, A., 2015 (Accepted for publication). SwiftScan: Efficient Wi-Fi scanning for background location-based services
    Doi: 10.17863/CAM.43449
    •

    2015

  • Snee, J., Carata, L., Chick, ORA., Sohan, R., Faragher, RM., Rice, A. and Hopper, A., 2015. Soroban: Attributing latency in virtualized environments 7th USENIX Workshop on Hot Topics in Cloud Computing, HotCloud 2015,
    •
  • Snee, J., Carata, L., Chick, ORA., Sohan, R., Faragher, RM., Rice, A. and Hopper, A., 2015. Soroban: Attributing latency in virtualized environments 7th Usenix Workshop on Hot Topics in Cloud Computing Hotcloud 2015,
    •
  • Cummins, S., Davies, I., Rice, A. and Beresford, AR., 2015. Equality: A tool for free-form equation editing Proceedings IEEE 15th International Conference on Advanced Learning Technologies Advanced Technologies for Supporting Open Access to Formal and Informal Learning Icalt 2015,
    Doi: 10.1109/ICALT.2015.34
    •
  • Thomas, DR., Beresford, AR. and Rice, A., 2015. Security metrics for the Android ecosystem SPSM 2015 - Proceedings of the 5th Annual ACM CCS Workshop on Security and Privacy in Smartphones and Mobile Devices, co-located with: CCS 2015,
    Doi: 10.1145/2808117.2808118
    •
  • Snee, J., Carata, L., Chick, ORA., Sohan, R., Faragher, RM., Rice, A. and Hopper, A., 2015. Soroban: Attributing latency in virtualized environments 7th USENIX Workshop on Hot Topics in Cloud Computing, HotCloud 2015,
    •
  • Wagner, DT., Thomas, DR., Beresford, AR. and Rice, A., 2015. Device analyzer: A privacy-aware platform to support research on the android ecosystem Proceedings of the 8th ACM Conference on Security and Privacy in Wireless and Mobile Networks Wisec 2015,
    Doi: 10.1145/2766498.2774992
    •

    2014

  • Rice, A. and Beresford, AR., 2014. The device analyzer competition Ubicomp 2014 Adjunct Proceedings of the 2014 ACM International Joint Conference on Pervasive and Ubiquitous Computing,
    Doi: 10.1145/2638728.2641696
    •
  • Wagner, DT., Rice, A. and Beresford, AR., 2014. Device analyzer: Understanding smartphone usage Lecture Notes of the Institute for Computer Sciences Social Informatics and Telecommunications Engineering Lnicst, v. 131
    Doi: 10.1007/978-3-319-11569-6_16
    •

    2013 (Accepted for publication)

  • Ding, N., Wagner, D., Chen, X., Pathak, A., Hu, YC. and Rice, AC., 2013 (Accepted for publication). Characterizing and modeling the impact of wireless signal strength on smartphone battery drain Proceedings of the ACM SIGMETRICS/international conference on Measurement and modeling of computer systems,
    Doi: 10.1145/2465529.2466586
    •

    2013

  • Carata, L., Sohan, R., Rice, A. and Hopper, A., 2013. IPAPI: Designing an improved provenance API 5th Workshop on the Theory and Practice of Provenance Tapp 2013,
    •
  • Ding, N., Wagner, D., Chen, X., Hu, YC. and Rice, A., 2013. Characterizing and modeling the impact of wireless signal strength on smartphone battery drain Performance Evaluation Review, v. 41
    Doi: 10.1145/2494232.2466586
    •

    2011

  • Rice, A. and Turner, SJ., 2011. Message from the MASCOTS 2011 program chairs IEEE International Workshop on Modeling Analysis and Simulation of Computer and Telecommunication Systems Proceedings,
    Doi: 10.1109/MASCOTS.2011.5
    •
  • Beresford, AR., Rice, A., Skehin, N. and Sohan, R., 2011. MockDroid: trading privacy for application functionality on smartphones In the Proceedings of the 11th Workshop on Mobile Computing Systems and Applications (HotMobile),
    •
  • Akoush, S., Sohan, R., Rice, A., Moore, AW. and Hopper, A., 2011. Free lunch: Exploiting renewable energy for computing 13th Workshop on Hot Topics in Operating Systems Hotos 2011,
    •
  • Sohan, RS., Akoush, SA., Rice, AC., Moore, AW. and Hopper, A., 2011. Free Lunch: Exploiting Renewable Energy For Computing

    • 2010

  • Rice, AC. and Hay, S., 2010. Decomposing power measurements for mobile devices. PerCom,
    Doi: 10.1109/PERCOM.2010.5466991
    •
  • Rice, AC. and Woodman, OJ., 2010. Crowd-sourcing world models with OpenRoomMap. PerCom Workshops,
    Doi: 10.1109/PERCOMW.2010.5470536
    •
  • Rice, A., Hay, S. and Ryder-Cook, D., 2010. A limited-data model of building energy consumption Proceedings of the 2nd ACM Workshop on Embedded Sensing Systems for Energy-Efficiency in Building - BuildSys ’10,
    Doi: 10.1145/1878431.1878447
    •
  • Vallina-Rodriguez, N., Hui, P., Crowcroft, J. and Rice, AC., 2010. Exhausting battery statistics: understanding the energy demands on mobile handsets. MobiHeld,
    •
  • Akoush, S., Sohan, R., Rice, A., Moore, AW. and Hopper, A., 2010. Predicting the performance of virtual machine migration Proceedings 18th Annual IEEE ACM International Symposium on Modeling Analysis and Simulation of Computer and Telecommunication Systems Mascots 2010,
    Doi: 10.1109/MASCOTS.2010.13
    •
  • Sohan, R., Rice, A., Moore, AW. and Mansley, K., 2010. Characterizing 10 Gbps network interface energy consumption Proceedings Conference on Local Computer Networks LCN,
    Doi: 10.1109/LCN.2010.5735719
    •

    2009

  • Hay, S. and Rice, A., 2009. The case for apportionment Proceedings of the First ACM Workshop on Embedded Sensing Systems for Energy-Efficiency in Buildings - BuildSys ’09,
    Doi: 10.1145/1810279.1810283
    •

    2008

  • Hylick, A., Sohan, R., Rice, AC. and Jones, B., 2008. An Analysis of Hard Drive Energy Consumption. MASCOTS,
    •
  • Hopper, A. and Rice, A., 2008. Computing for the future of the planet. Philos Trans A Math Phys Eng Sci, v. 366
    Doi: 10.1098/rsta.2008.0124
    •

    2006

  • Rice, AC., Beresford, AR. and Harle, RK., 2006. Cantag: An open source software toolkit for designing and deploying marker-based vision systems PERCOM 2006: FOURTH ANNUAL IEEE INTERNATIONAL CONFERENCE ON PERVASIVE COMPUTING AND COMMUNICATIONS, PROCEEDINGS,
    •
  • Rice, AC. and Beresford, AR., 2006. Dependability and accountability for context-aware middleware systems FOURTH ANNUAL IEEE INTERNATIONAL CONFERENCE ON PERVASIVE COMPUTING AND COMMUNICATIONS WORKSHOPS, PROCEEDINGS,
    •
  • Rice, AC., Harle, RK. and Beresford, AR., 2006. Analysing fundamental properties of marker-based vision system designs. Pervasive Mob. Comput., v. 2
    Doi: 10.1016/j.pmcj.2006.07.006
    •

    2005

  • Rice, AC. and Harle, RK., 2005. Evaluating lateration-based positioning algorithms for fine-grained tracking. DIALM-POMC,
    •
  • Rice, AC., Cain, CB. and Fawcett, JK., 2005. Dependable coding of fiducial tags UBIQUITOUS COMPUTING SYSTEMS, v. 3598
    •
    Datasets

    2019

  • Rice, AC. and Licker, N., 2019. Detecting Incorrect Build Rules - Artifact
    Doi: 10.17863/CAM.35270
    •

    2017

  • Orchard, D., Contrastin, M., Danish, M. and Rice, AC., 2017. Research data supporting Verifying Spatial Properties of Array Computations
    Doi: 10.17863/CAM.12627
    •

    2015 (No publication date)

  • Thomas, DR., Wagner, DT., Beresford, AR. and Rice, A., 2015 (No publication date). Supporting data for: "Security metrics for the Android ecosystem"
    • Book chapters

    2012

  • Audzevich, Y., Moore, AW., Rice, AC., Sohan, R., Timotheou, S., Crowcroft, J., Akoush, S., Hopper, A., Wonfor, A., Wang, H., Penty, RV., White, IH., Dong, X., El-Gorashi, TEH. and Elmirghani, JMH., 2012. Intelligent Energy-Aware Networks.
    • Read more at: Paul Scherer

    Paul Scherer

    Read more at: Dr Vadim Safronov

    Dr Vadim Safronov

    Visiting Researcher in the Department of Computer Science and Technology, University of Cambridge.

    Research Associate at the Department of Computer Science, University of Oxford. PhD in Computer Science, University of Cambridge.

    Read more at: Dr Daniel Raggi

    Dr Daniel Raggi

    Read more at: Diana Robinson

    Diana Robinson

    Read more at: Prof Amanda Prorok

    Prof Amanda Prorok

    Amanda Prorok is Professor of Collective Intelligence and Robotics in the Department of Computer Science and Technology, at Cambridge University, and a Fellow of Pembroke College.

    Read more at: Dr Zohreh Shams

    Dr Zohreh Shams

    Please visit my personal homepage for more information :)

    Read more at: Dr Thomas Sauerwald

    Dr Thomas Sauerwald

    Read more at: Lawrence C Paulson FRS

    Lawrence C Paulson FRS

     

    Conference proceedings

  • Edmonds, C. and Paulson, LC., 2024. Formal Probabilistic Methods for Combinatorial Structures using the Lovász Local Lemma Cpp 2024 Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs Co Located with Popl 2024,
    Doi: 10.1145/3636501.3636946
    •
  • Eberl, M., Bordg, A., Paulson, LC. and Li, W., 2024. Formalising Half of a Graduate Textbook on Number Theory Leibniz International Proceedings in Informatics Lipics, v. 309
    Doi: 10.4230/LIPIcs.ITP.2024.40
    •
  • Edmonds, C. and Paulson, LC., 2022. Formalising Fisher's Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics Leibniz International Proceedings in Informatics Lipics, v. 237
    Doi: 10.4230/LIPIcs.ITP.2022.11
    •
  • Mangla, C., Holden, SB. and Paulson, LC., 2022. Bayesian Ranking for Strategy Scheduling in Automated Theorem Provers Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, v. 13385 LNAI
    Doi: 10.1007/978-3-031-10769-6_33
    •
  • Paulson, LC., 2022. Wetzel: Formalisation of an Undecidable Problem Linked to the Continuum Hypothesis. CICM, v. 13467
    •
  • Edmonds, C. and Paulson, LC., 2022. Formalising Fisher's Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics 13th International Conference on Interactive Theorem Proving (2022). 11:1-11:19,
    •
  • Edmonds, C. and Paulson, LC., 2021. A Modular First Formalisation of Combinatorial Design Theory Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, v. 12833 LNAI
    Doi: 10.1007/978-3-030-81097-9_1
    •
  • Li, W., Yu, L., Wu, Y. and Paulson, LC., 2021. ISARSTEP: A BENCHMARK FOR HIGH-LEVEL MATHEMATICAL REASONING Iclr 2021 9th International Conference on Learning Representations,
    •
  • Edmonds, C. and Paulson, LC., 2021. A Modular First Formalisation of Combinatorial Design Theory. CICM, v. 12833
    •
  • Słowik, A., Mangla, C., Jamnik, M., Holden, S. and Paulson, L., 2020 (No publication date). Bayesian Optimisation for Heuristic Configuration in Automated Theorem Proving EPiC Series in Computing, v. 71
    Doi: 10.29007/q91g
    •
  • de Vilhena, PE. and Paulson, L., 2020 (Accepted for publication). Algebraically Closed Fields in Isabelle/HOL Automated Reasoning—10th International Joint Conference, IJCAR 2020,
    Doi: 10.1007/978-3-030-51054-1_12
    •
  • Slowik, A., Mangla, C., Jamnik, M., Holden, SB. and Paulson, LC., 2020. Bayesian Optimisation for Premise Selection in Automated Theorem Proving (Student Abstract). Proceedings of the AAAI Conference on Artificial Intelligence, 34(10), v. 34
    Doi: 10.1609/aaai.v34i10.7232
    •
  • Mangla, C., Holden, SB. and Paulson, LC., 2020. Bayesian optimisation of solver parameters in CBMC Ceur Workshop Proceedings, v. 2854
    •
  • 2020. Automated Reasoning
    Doi: 10.1007/978-3-030-51074-9
    •
  • Słowik, A., Mangla, C., Jamnik, M., Holden, SB. and Paulson, LC., 2020. Bayesian optimisation for premise selection in automated theorem proving (student abstract) Aaai 2020 34th Aaai Conference on Artificial Intelligence,
    •
  • Li, W. and Paulson, LC., 2019. Counting polynomial roots in Isabelle/HOL: A formal proof of the Budan-Fourier theorem Cpp 2019 Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs Co Located with Popl 2019,
    Doi: 10.1145/3293880.3294092
    •
  • Li, W. and Paulson, LC., 2018 (Accepted for publication). Counting Polynomial Roots in Isabelle/HOL: A Formal Proof of the Budan-Fourier Theorem Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs,
    Doi: 10.1145/3293880.3294092
    •
  • Huang, Z., England, M., Davenport, JH. and Paulson, LC., 2017. Using machine learning to decide when to precondition cylindrical algebraic decomposition with groebner bases Proceedings - 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2016,
    Doi: 10.1109/SYNASC.2016.020
    •
  • Paulson, LC., 2017. Porting the HOL Light Analysis Library: Some Lessons (Invited Talk) PROCEEDINGS OF THE 6TH ACM SIGPLAN CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP'17,
    Doi: 10.1145/3018610.3023366
    •
  • Li, W. and Paulson, LC., 2016. A modular, efficient formalisation of real algebraic numbers Cpp 2016 Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs Co Located with Popl 2016,
    Doi: 10.1145/2854065.2854074
    •
  • Huang, Z., England, M., Davenport, JH. and Paulson, LC., 2016. Using Machine Learning to Decide When to Precondition Cylindrical Algebraic Decomposition With Groebner Bases PROCEEDINGS OF 2016 18TH INTERNATIONAL SYMPOSIUM ON SYMBOLIC AND NUMERIC ALGORITHMS FOR SCIENTIFIC COMPUTING (SYNASC),
    Doi: 10.1109/SYNASC.2016.14
    •
  • Sultana, N., Benzmüller, C. and Paulson, LC., 2015. Proofs and reconstructions Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, v. 9322
    Doi: 10.1007/978-3-319-24246-0_16
    •
  • Huang, Z., England, M., Wilson, D., Davenport, JH. and Paulson, LC., 2015. A comparison of three heuristics to choose the variable ordering for cylindrical algebraic decomposition ACM Communications in Computer Algebra, v. 48
    Doi: 10.1145/2733693.2733706
    •
  • Paulson, LC., 2015. A formalisation of finite automata using hereditarily finite sets Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, v. 9195
    Doi: 10.1007/978-3-319-21401-6_15
    •
  • Jackson, P., Sogokon, A., Bridge, J. and Paulson, L., 2014. Verifying hybrid systems involving transcendental functions Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, v. 8430 LNCS
    Doi: 10.1007/978-3-319-06200-6_14
    •
  • Paulson, LC., 2013. MetiTarski's Menagerie of Cooperating Systems. FroCos, v. 8152
    •
  • Paulson, LC., 2012. MetiTarski: Past and Future. ITP, v. 7406
    •
  • Paulson, LC. and Susanto, KW., 2010 (No publication date). Source-Level Proof Reconstruction for Interactive Theorem Proving
  • Meng, J. and Paulson, LC., 2010 (No publication date). Translating Higher-Order Problems to First-Order Clauses
  • Meng, J. and Paulson, LC., 2010 (No publication date). Lightweight Relevance Filtering for Machine-Generated Resolution Problems
  • Narayanan, R., Akbarpour, B., Zaki, MH., Tahar, S. and Paulson, LC., 2010. Formal verification of analog circuits in the presence of noise and process variation. DATE,
    •
  • 2010. Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings ITP, v. 6172
    •
  • Paulson, LC. and Blanchette, JC., 2010. Three years of experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers. IWIL@LPAR, v. 2
    •
  • Paulson, LC., 2010. Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem Provers. PAAR@IJCAR, v. 9
    •
  • Akbarpour, B. and Paulson, LC., 2009. Applications of MetiTarski in the Verification of Control and Hybrid Systems. HSCC, v. 5469
    •
  • Akbarpour, B. and Paulson, LC., 2009. Applications of MetiTarski in the Verification of Control and Hybrid Systems HYBRID SYSTEMS: COMPUTATION AND CONTROL, v. 5469
    •
  • Akbarpour, B. and Paulson, LC., 2009. Applications of MetiTarski in the Verification of Control and Hybrid Systems Hybrid Systems: Computation and Control,
    •
  • Denman, W., Akbarpour, B., Tahar, S., Zaki, M. and Paulson, LC., 2009. Formal Verification of Analog Designs using MetiTarski Formal Methods in Computer Aided Design,
    Doi: 10.1109/FMCAD.2009.5351136
    •
  • Benzmüller, C. and Paulson, LC., 2009. Quantified Multimodal Logics in Simple Type Theory CoRR, v. abs/0905.2435
    •
  • Wenzel, M., Paulson, LC. and Nipkow, T., 2008. The Isabelle Framework Theorem Proving in Higher Order Logics: TPHOLs 2008,
    Doi: 10.1007/978-3-540-71067-7_7
    •
  • Paulson, LC., 2008. The relative consistency of the axiom of choice - Mechanized using Isabelle/ZF LOGIC AND THEORY OF ALGORITHMS, v. 5028
    •
  • Benzmüller, C., Paulson, LC., Theiss, F. and Fietzke, A., 2008. LEO-II - A Cooperative Automatic Theorem Prover for Higher-Order Logic Automated Reasoning — 4th International Joint Conference, IJCAR 2008,
    Doi: 10.1007/978-3-540-71070-7_14
    •
  • Meng, J., Paulson, LC. and Klein, G., 2007. A Termination Checker for Isabelle Hoare Logic 4th International Verification Workshop - VERIFY’07, v. 259
    •
  • Akbarpour, B. and Paulson, L., 2007. Extending a Resolution Prover for Inequalities on Elementary Functions Logic for Programming, Artificial Intelligence, and Reasoning,
    Doi: 10.1007/978-3-540-75560-9_6
    •
  • Akbarpour, B. and Paulson, LC., 2006. Towards Automatic Proofs of Inequalities Involving Elementary Functions PDPAR: Pragmatics of Decision Procedures in Automated Reasoning,
    •
  • 2006. FLoC’06 Workshop on Empirically Successful Computerized Reasoning
  • Wenzel, M. and Paulson, LC., 2006. Isabelle/Isar.
  • Nipkow, T. and Paulson, LC., 2005. Proof pearl: Defining functions over finite sets THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS, v. 3603
    •
  • Bella, G., Longo, C. and Paulson, LC., 2005. Is the verification problem for cryptographic protocols solved? SECURITY PROTOCOLS, v. 3364
    •
  • Nipkow, T. and Paulson, LC., 2005. Proof Pearl: Defining Functions Over Finite Sets Theorem Proving in Higher Order Logics: TPHOLs 2005,
    Doi: 10.1007/11541868_25
    •
  • Bella, G. and Paulson, LC., 2004. Analyzing delegation properties SECURITY PROTOCOLS, v. 2845
    •
  • Meng, J. and Paulson, LC., 2004. Experiments on supporting interactive proof using resolution AUTOMATED REASONING, PROCEEDINGS, v. 3097
    •
  • Meng, J. and Paulson, LC., 2004. Experiments On Supporting Interactive Proof Using Resolution Automated Reasoning — Second International Joint Conference, IJCAR 2004,
    Doi: 10.1007/b98691
    •
  • Paulson, LC., 2004. The descent of BAN COMPUTER SYSTEMS: THEORY, TECHNOLOGY AND APPLICATIONS,
    •
  • Bella, G., Longo, C. and Paulson, LC., 2003. Verifying Second-Level Security Protocols Theorem Proving in Higher Order Logics: TPHOLs 2003,
    •
  • Paulson, LC., 2003. Verifying the SET protocol: Overview FORMAL ASPECTS OF SECURITY, v. 2629
    •
  • Bella, G., Paulson, LC. and Massacci, F., 2002. The verification of an industrial payment protocol: the SET purchase phase. CCS,
    •
  • Ehmety, SO. and Paulson, LC., 2002. Program Composition in Isabelle/UNITY Workshop on Formal Methods for Parallel Programming: Theory and Applications; text on CD-ROM,
    •
  • Bella, G. and Paulson, LC., 2002. A proof of non-repudiation SECURITY PROTOCOLS, v. 2467
    •
  • Paulson, L., 2002. A proof of non-repudiation - (Transcript of discussion) SECURITY PROTOCOLS, v. 2467
    •
  • Christianson, B., Aura, T., Wheeler, D., Harbison, W., Gligor, V., Paulson, L., Blaze, M. and Ioannidis, J., 2002. Concluding discussion - When does confidentiality harm security? SECURITY PROTOCOLS, v. 2467
    •
  • Paulson, LC., 2002. The Reflection Theorem: A Study in Meta-theoretic Reasoning. CADE, v. 2392
    •
  • Bella, G., Massacci, F., Paulson, LC. and Tramontano, P., 2001. Making sense of specifications: The formalization of SET (Extended abstract) Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, v. 2133
    Doi: 10.1007/3-540-44810-1_11
    •
  • Bella, G. and Paulson, LC., 2001. Mechanical Proofs about a Non-repudiation Protocol. TPHOLs, v. 2152
    •
  • Paulson, LC., 2001. SET Cardholder Registration: The Secrecy Proofs. IJCAR, v. 2083
    •
  • Bella, G., Massacci, F., Paulson, LC. and Tramontano, P., 2000. Formal Verification of Cardholder Registration in SET Computer Security — ESORICS 2000,
    •
  • Paulson, LC., 2000. Relations between secrets: The yahalom protocol extended abstract Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, v. 1796
    Doi: 10.1007/10720107_10
    •
  • Bella, G., Massacci, F., Paulson, LC. and Tramontano, P., 2000. Making Sense of Specifications: The Formalization of SET. Security Protocols Workshop, v. 2133
    •
  • Paulson, LC., 2000. Making Sense of Specifications: The Formalization of SET (Transcript of Discussion). Security Protocols Workshop, v. 2133
    •
  • Paulson, LC., 2000. Relations between secrets: The Yahalom protocol SECURITY PROTOCOLS, v. 1796
    •
  • Paulson, LC., 2000. The Yahalom protocol SECURITY PROTOCOLS, v. 1796
    •
  • Bella, G., Massacci, F., Paulson, LC. and Tramontano, P., 2000. Formal verification of Cardholder Registration in SET COMPUTER SECURITY - ESORICS 2000, PROCEEDINGS, v. 1895
    •
  • Paulson, LC., 1999. Proving Security Protocols Correct. LICS,
    Doi: 10.1109/LICS.1999.782632
    •
  • Fleuriot, J. and Paulson, LC., 1999. Proving Newton’s Propositio Kepleriana Using Geometry and Nonstandard Analysis in Isabelle Workshop on Automated Deduction in Geometry, Second International Workshop, ADG’98,
    •
  • Kammüller, F., Wenzel, M. and Paulson, LC., 1999. Locales: A Sectioning Concept for Isabelle Theorem Proving in Higher Order Logics: TPHOLs ’99,
    •
  • Ballarin, C. and Paulson, LC., 1998. Reasoning about coding theory: The benefits we get from computer algebra Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), v. 1476
    •
  • Paulson, LC., 1998. Inductive Analysis of the Internet Protocol TLS (Position Paper). Security Protocols Workshop, v. 1550
    •
  • Paulson, LC., 1998. A Generic Tableau Prover and its Integration with Isabelle (Extended Abstract) CADE-15 Workshop on Integration of Deduction Systems,
    •
  • Paulson, LC., 1998. Inductive Analysis of the Internet Protocol TLS (Transcript of Discussion). Security Protocols Workshop, v. 1550
    •
  • Bella, G. and Paulson, LC., 1998. Kerberos Version IV: Inductive Analysis of the Secrecy Goals Computer Security — ESORICS 98,
    •
  • Paulson, L., 1998. Inductive analysis of the internet protocol TLS Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, v. 1550
    Doi: 10.1007/3-540-49135-X_2
    •
  • Bella, G. and Paulson, LC., 1998. Mechanising BAN Kerberos by the Inductive Method Computer Aided Verification: 10th International Conference, CAV ’98,
    •
  • Ballarin, C. and Paulson, LC., 1998. Reasoning About Coding Theory: The Benefits We Get from Computer Algebra. AISC, v. 1476
    •
  • Fleuriot, J. and Paulson, LC., 1998. A Combination of Nonstandard Analysis and Geometry Theorem Proving, with Application to Newton’s Principia Automated Deduction — CADE-15 International Conference,
    •
  • Paulson, LC., 1997. Mechanizing Coinduction and Corecursion in Higher-Order Logic. J. Log. Comput., v. 7
    Doi: 10.1093/logcom/7.2.175
    •
  • Paulson, LC., 1997. Proving Properties of Security Protocols by Induction 10th Computer Security Foundations Workshop,
    •
  • Paulson, LC., 1997. Mechanized Proofs for a Recursive Authentication Protocol 10th Computer Security Foundations Workshop,
    •
  • Bella, G. and Paulson, LC., 1997. Using Isabelle to Prove Properties of the Kerberos Authentication System Workshop on Design and Formal Verification of Security Protocols,
    •
  • 1995. First Isabelle Users Workshop
  • Paulson, LC., 1994. A Concrete Final Coalgebra Theorem for ZF Set Theory. TYPES, v. 996
    •
  • Paulson, LC., 1994. A Fixedpoint Approach to Implementing (Co)Inductive Definitions Automated Deduction — CADE-12,
    •
  • Paulson, LC., 1993. A Formulation of the Simple Theory of Types (for Isabelle) CoRR, v. cs.LO/9301107
    •
  • Nipkow, T. and Paulson, LC., 1992. Isabelle-91 (system abstract) Automated Deduction — CADE-11,
    •
  • NIPKOW, T. and PAULSON, LC., 1992. ISABELLE-91 AUTOMATED DEDUCTION - CADE-11, v. 607
    •
  • Paulson, LC. and Smith, AW., 1991. Logic Programming, Functional Programming, and Inductive Definitions Extensions of Logic Programming,
    •
  • Paulson, LC., 1990. A Formulation of the Simple Theory of Types (for Isabelle) COLOG-88: International Conference on Computer Logic,
    •
  • Paulson, LC. and Smith, AW., 1989. Logic Programming, Functional Programming, and Inductive Definitions. ELP, v. 475
    •
  • Paulson, LC., 1988. Isabelle: The Next Seven Hundred Theorem Provers. CADE, v. 310
    •
  • Paulson, LC., 1987. NEXT SEVEN HUNDRED THEOREM PROVERS. IEE Colloquium Digest,
    •
  • Paulson, LC., 1986. Natural Deduction as Higher-Order Resolution. J. Log. Program., v. 3
    Doi: 10.1016/0743-1066(86)90015-4
    •
  • Paulson, LC., 1985. Verifying the Unification Algorithm in LCF. Sci. Comput. Program., v. 5
    Doi: 10.1016/0167-6423(85)90009-7
    •
  • Paulson, LC., 1984. Deriving Structural Induction in LCF. Semantics of Data Types, v. 173
    •
  • Paulson, LC., 1983. A Higher-Order Implementation of Rewriting. Sci. Comput. Program., v. 3
    Doi: 10.1016/0167-6423(83)90008-4
    •
  • Paulson, LC., 1983. Compiler Generation from Denotational Semantics. Method and tools for compiler construction,
    •
  • Paulson, LC., 1982. A Semantics-Directed Compiler Generator. POPL,
    •
  • Paulson, L., 1982. A Semantics-Directed Compiler Generator Ninth Annual ACM Symposium on Principles of Programming Languages,
    •

    Journal articles

  • Edmonds, C., Koutsoukou-Argyraki, A. and Paulson, LC., 2023. Formalising Szemerédi’s Regularity Lemma and Roth’s Theorem on Arithmetic Progressions in Isabelle/HOL Journal of Automated Reasoning, v. 67
    Doi: 10.1007/s10817-022-09650-2
    •
  • Paulson, LC., 2022 (Accepted for publication). A Formalised Theorem in the Partition Calculus Annals of Pure and Applied Logic,
    •
  • Bordg, A., Paulson, L. and Li, W., 2022 (Accepted for publication). Simple Type Theory is not too Simple: Grothendieck’s Schemes Without Dependent Types Experimental Mathematics, v. 31
    Doi: 10.1080/10586458.2022.2062073
    •
  • Bayer, J., Benzmüller, C., Buzzard, K., David, M., Lamport, L., Matiyasevich, Y., Paulson, L., Schleicher, D., Stock, B. and Zelmanov, E., 2022. Mathematical Proof Between Generations Notices of the American Mathematical Society, v. 71
    •
  • Coward, S., Paulson, L., Drane, T. and Morini, E., 2022. Formal Verification of Transcendental Fixed- and Floating-point Algorithms using an Automatic Theorem Prover Formal Aspects of Computing, v. 34
    Doi: 10.1145/3543670
    •
  • Džamonja, M., Koutsoukou-Argyraki, A. and Paulson, LC., 2021 (Accepted for publication). Formalising Ordinal Partition Relations Using Isabelle/HOL Experimental Mathematics,
    •
  • Paulson, LC., 2021 (Accepted for publication). Ackermann's Function in Iterative Form: A Proof Assistant Experiment Bulletin of Symbolic Logic,
    •
  • Koutsoukou-Argyraki, A., Li, W. and Paulson, LC., 2021 (Accepted for publication). Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL Experimental Mathematics,
    •
  • Paulson, LC., 2021. The Inductive Approach to Verifying Cryptographic Protocols. CoRR, v. abs/2105.06319
    •
  • Bordg, A., Paulson, LC. and Li, W., 2021. Grothendieck's Schemes in Algebraic Geometry. Arch. Formal Proofs, v. 2021
    •
  • Paulson, LC., 2020. The Nash-Williams Partition Theorem. Arch. Formal Proofs, v. 2020
    •
  • Li, W., Yu, L., Wu, Y. and Paulson, LC., 2020. Modelling High-Level Mathematical Reasoning in Mechanised Declarative Proofs. CoRR, v. abs/2006.09265
    •
  • Paulson, LC., 2020. Ordinal Partitions. Arch. Formal Proofs, v. 2020
    •
  • Li, W. and Paulson, LC., 2020. Evaluating Winding Numbers and Counting Complex Roots Through Cauchy Indices in Isabelle/HOL. J. Autom. Reasoning, v. 64
    Doi: 10.1007/s10817-019-09521-3
    •
  • Huang, Z., England, M., Wilson, D., Davenport, JH. and Paulson, LC., 2019 (Accepted for publication). Using Machine Learning to Improve Cylindrical Algebraic Decomposition Mathematics in Computer Science,
    Doi: 10.1007/s11786-019-00394-8
    •
  • Abdulaziz, M. and Paulson, LC., 2019. An Isabelle/HOL Formalisation of Green’s Theorem Journal of Automated Reasoning, v. 63
    Doi: 10.1007/s10817-018-9495-z
    •
  • Paulson, LC., Nipkow, T. and Wenzel, M., 2019. From LCF to Isabelle/HOL Formal Aspects of Computing, v. 31
    Doi: 10.1007/s00165-019-00492-1
    •
  • Paulson, LC., 2019. Formalising Mathematics in Simple Type Theory
    Doi: 10.1007/978-3-030-15655-8_20
    •
  • Słowik, A., Mangla, C., Jamnik, M., Holden, SB. and Paulson, LC., 2019. Bayesian Optimisation with Gaussian Processes for Premise Selection
  • Paulson, LC., 2019. Zermelo Fraenkel Set Theory in Higher-Order Logic. Arch. Formal Proofs, v. 2019
    •
  • Huang, Z., England, M., Wilson, DJ., Bridge, JP., Davenport, JH. and Paulson, LC., 2019. Using Machine Learning to Improve Cylindrical Algebraic Decomposition. Math. Comput. Sci., v. 13
    •
  • Paulson, LC., 2019. Fourier Series. Arch. Formal Proofs, v. 2019
    •
  • Li, W., Passmore, GO. and Paulson, LC., 2019. Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle/HOL JOURNAL OF AUTOMATED REASONING, v. 62
    Doi: 10.1007/s10817-017-9424-6
    •
  • Paulson, L., Nipkow, T. and Wenzel, M., 2019. From LCF to Isabelle/HOL Formal Aspects of Computing, v. 31
    Doi: 10.1007/s00165-019-00492-1
    •
  • Paulson, LC., 2018 (Accepted for publication). Computational Logic: Its Origins and Applications Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences,
    •
  • Paulson, LC., 2018. Predicting Failure of the University COMMUNICATIONS OF THE ACM, v. 61
    •
  • Avigad, J., Blanchette, JC., Klein, G., Paulson, L., Popescu, A. and Snelting, G., 2018. Introduction to Milestones in Interactive Theorem Proving Journal of Automated Reasoning, v. 61
    Doi: 10.1007/s10817-018-9465-5
    •
  • Paulson, LC., 2018. Michael John Caldwell Gordon (FRS 1994), 28 February 1948 -- 22 August 2017 Biographical memoirs of fellows of the Royal Society. Royal Society (Great Britain), v. 65
    Doi: 10.1098/rsbm.2018.0019
    •
  • Eberl, M. and Paulson, LC., 2018. The Prime Number Theorem. Arch. Formal Proofs, v. 2018
    •
  • Li, W., Passmore, G. and Paulson, LC., 2017 (Accepted for publication). Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle/HOL Journal of Automated Reasoning,
    Doi: 10.1007/s10817-017-9424-6
    •
  • Paulson, LC., 2017. Time to Retire 'Computational Thinking'? COMMUNICATIONS OF THE ACM, v. 60
    •
  • Blanchette, JC., Kaliszyk, C., Paulson, LC. and Urban, J., 2016. Hammering towards QED Journal of Formalized Reasoning, v. 9
    •
  • Hibon, Q. and Paulson, LC., 2016. Source Coding Theorem. Arch. Formal Proofs, v. 2016
    •
  • Paulson, LC., 2016. The Cartan Fixed Point Theorems. Arch. Formal Proofs, v. 2016
    •
  • Abdulaziz, M. and Paulson, LC., 2016. An Isabelle/HOL formalisation of Green’s theorem Lecture Notes in Computer Science, v. 9807
    Doi: 10.1007/978-3-319-43144-4_1
    •
  • Li, W. and Paulson, LC., 2016. A formal proof of Cauchy’s residue theorem Lecture Notes in Computer Science, v. 9807
    Doi: 10.1007/978-3-319-43144-4_15
    •
  • Paulson, LC., 2015. A Mechanised Proof of Gödel’s Incompleteness Theorems Using Nominal Isabelle Journal of Automated Reasoning, v. 55
    Doi: 10.1007/s10817-015-9322-8
    •
  • Benzmüller, C., Sultana, N., Paulson, LC. and Theiß, F., 2015. The Higher-Order Prover Leo-II. J Autom Reason, v. 55
    Doi: 10.1007/s10817-015-9348-y
    •
  • Paulson, LC., 2015. Finite Automata in Hereditarily Finite Set Theory. Arch. Formal Proofs, v. 2015
    •
  • Paulson, LC., 2015. A Mechanised Proof of Gödel’s Incompleteness Theorems Using Nominal Isabelle Journal of Automated Reasoning,
    Doi: 10.1007/s10817-015-9322-8
    •
  • Paulson, LC., 2015. A Formalisation of Finite Automata using Hereditarily Finite Sets. CoRR, v. abs/1505.01662
    •
  • Paulson, LC., 2015. Abolish Software Warranty Disclaimers COMMUNICATIONS OF THE ACM, v. 58
    •
  • Martina, JE. and Paulson, LC., 2015. Verifying multicast-based security protocols using the inductive method International Journal of Information Security, v. 14
    Doi: 10.1007/s10207-014-0251-z
    •
  • Paulson, LC., 2014. Automated theorem proving for special functions: The next phase Proceedings of the 2014 Symposium on Symbolic Numeric Computation Snc 2014,
    Doi: 10.1145/2631948.2631950
    •
  • Paulson, LC., 2014. A machine-assisted proof of Gödel's incompleteness theorems for the theory of hereditarily finite sets Review of Symbolic Logic, v. 7
    Doi: 10.1017/S1755020314000112
    •
  • Paulson, LC., 2014. Provenance of British Computing COMMUNICATIONS OF THE ACM, v. 57
    •
  • Huang, Z., England, M., Wilson, D., Davenport, JH. and Paulson, LC., 2014. A comparison of three heuristics to choose the variable ordering for CAD ACM Communications in Computer Algebra 48:3 (issue 189), pp. 121-123, ACM, 2014,
    •
  • Paulson, LC., 2014. Real-Valued Special Functions: Upper and Lower Bounds. Arch. Formal Proofs, v. 2014
    •
  • PAULSON, LC., 2014. A MACHINE-ASSISTED PROOF OF GÖDEL'S INCOMPLETENESS THEOREMS FOR THE THEORY OF HEREDITARILY FINITE SETS Review of Symbolic Logic,
    Doi: 10.1017/S1755020314000112
    •
  • Bridge, JP., Holden, SB. and Paulson, LC., 2014. Machine Learning for First-Order Theorem Proving Journal of Automated Reasoning,
    •
  • Paulson, LC., 2014. Theorem proving and the real numbers: Overview and challenges Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, v. 8430 LNCS
    •
  • Bridge, JP., Holden, SB. and Paulson, LC., 2014. Machine learning for first-order theorem proving: Learning to select a good Heuristic Journal of Automated Reasoning, v. 53
    Doi: 10.1007/s10817-014-9301-5
    •
  • Huang, Z., England, M., Wilson, D., Davenport, JH., Paulson, LC. and Bridge, J., 2014. Applying machine learning to the problem of choosing a heuristic to select the variable ordering for cylindrical algebraic decomposition Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, v. 8543 LNAI
    Doi: 10.1007/978-3-319-08434-3_8
    •
  • Huang, Z., England, M., Wilson, DJ., Davenport, JH., Paulson, LC. and Bridge, JP., 2014. Applying machine learning to the problem of choosing a heuristic to select the variable ordering for cylindrical algebraic decomposition. CoRR, v. abs/1404.6369
    •
  • Paulson, LC., 2013. What we want from computer science Communications of the ACM, v. 56
    Doi: 10.1145/2483852.2483856
    •
  • Bridge, JP. and Paulson, LC., 2013. Case splitting in an automatic theorem prover for real-valued special functions Journal of Automated Reasoning, v. 50
    Doi: 10.1007/s10817-012-9245-6
    •
  • Sultana, N., Blanchette, JC. and Paulson, LC., 2013. LEO-II and Satallax on the Sledgehammer test bench Journal of Applied Logic, v. 11
    Doi: 10.1016/j.jal.2012.12.002
    •
  • Blanchette, JC., Böhme, S. and Paulson, LC., 2013. Extending sledgehammer with SMT solvers Journal of Automated Reasoning, v. 51
    Doi: 10.1007/s10817-013-9278-5
    •
  • Benzmüller, C. and Paulson, LC., 2013. Quantified Multimodal Logics in Simple Type Theory Logica Universalis, v. 7
    Doi: 10.1007/s11787-012-0052-y
    •
  • Martina, JE. and Paulson, LC., 2013. Verifying multicast-based security protocols using the inductive method Proceedings of the ACM Symposium on Applied Computing,
    Doi: 10.1145/2480362.2480703
    •
  • Paulson, LC., 2013. The Hereditarily Finite Sets. Arch. Formal Proofs, v. 2013
    •
  • Paulson, LC., 2013. Gödel's Incompleteness Theorems. Arch. Formal Proofs, v. 2013
    •
  • Paulson, LC., 2012. What liability for faulty software? Communications of the ACM, v. 55
    Doi: 10.1145/2076450.2076452
    •
  • Romanos, R. and Paulson, LC., 2012. Proving the Impossibility of Trisecting an Angle and Doubling the Cube. Arch. Formal Proofs, v. 2012
    •
  • Blanchette, JC., Böhme, S. and Paulson, LC., 2011. Extending sledgehammer with SMT solvers Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, v. 6803 LNAI
    Doi: 10.1007/978-3-642-22438-6_11
    •
  • Akbarpour, B. and Paulson, LC., 2010. MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions J AUTOM REASONING, v. 44
    Doi: 10.1007/s10817-009-9149-2
    •
  • Paulson, LC., 2010. Robin Milner The Elegant Pragmatist (vol 53, pg 20, 2010) COMMUNICATIONS OF THE ACM, v. 53
    •
  • Benzmueller, C. and Paulson, LC., 2010. Multimodal and Intuitionistic Logics in Simple Type Theory Logic Jnl IGPL,
    Doi: 10.1093/jigpal/jzp080
    •
  • Meng, J. and Paulson, LC., 2009. Lightweight relevance filtering for machine-generated resolution problems J APPL LOGIC, v. 7
    Doi: 10.1016/j.jal.2007.07.004
    •
  • Paulson, LC., 2009. Refocus fragmented CS conference culture [3] Communications of the ACM, v. 52
    Doi: 10.1145/1536616.1536619
    •
  • Paulson, LC., 2009. Refocus Fragmented CS Conference Culture COMMUNICATIONS OF THE ACM, v. 52
    •
  • Akbarpour, B. and Paulson, LC., 2009. MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions Journal of Automated Reasoning,
    •
  • Akbarpour, B. and Paulson, L., 2008. MetiTarski: An Automatic Prover for the Elementary Functions Intelligent Computer Mathematics,
    •
  • Nipkow, T. and Paulson, LC., 2008. Fun With Tilings. Arch. Formal Proofs, v. 2008
    •
  • Meng, J. and Paulson, LC., 2008. Translating higher-order clauses to first-order clauses J AUTOM REASONING, v. 40
    Doi: 10.1007/s10817-007-9085-y
    •
  • Beckert, B. and Paulson, LC., 2007. Special issue on automated reasoning with analytic tableaux - Preface J AUTOM REASONING, v. 38
    Doi: 10.1007/s10817-006-9058-6
    •
  • Paulson, LC., 2007. Even a good abstraction needs experience and testing, too COMMUNICATIONS OF THE ACM, v. 50
    •
  • Beckert, B. and Paulson, LC., 2007. Journal of Automated Reasoning: Preface Journal of Automated Reasoning, v. 38
    Doi: 10.1007/s10817-006-9058-6
    •
  • Meng, J., Quigley, C. and Paulson, LC., 2006. Automation for interactive proof: First prototype INFORM COMPUT, v. 204
    Doi: 10.1016/j.ic.2005.05.010
    •
  • Bella, G. and Paulson, LC., 2006. Accountability protocols: Formalized and verified ACM Trans. Inf. Syst. Secur., v. 9
    Doi: 10.1145/1151414.1151416
    •
  • Paulson, LC., 2006. Defining Functions on Equivalence Classes TOCL, v. 7
    Doi: 10.1145/1166109.1166111
    •
  • Meng, J., Quigley, C. and Paulson, LC., 2006. Automation for interactive proof: First prototype (vol 204, pg 1575, 2006) INFORM COMPUT, v. 204
    Doi: 10.1016/j.ic.2006.09.004
    •
  • Meng, J., Quigley, C. and Paulson, LC., 2006. Automation for Interactive Proof: First Prototype Information and Computation, v. 204
    •
  • Paulson, LC., 2006. Defining functions on equivalence classes ACM Transactions on Computational Logic, v. 7
    Doi: 10.1145/1166109.1166111
    •
  • Meng, J., Quigley, C. and Paulson, LC., 2006. Erratum to "Automation for interactive proof: First prototype" [Inform. and Comput. 204 (2006) 1575-1596] (DOI:10.1016/j.ic.2005.05.010) Information and Computation, v. 204
    •
  • Bella, G., Massacci, F. and Paulson, LC., 2006. Verifying the SET purchase protocols J AUTOM REASONING, v. 36
    Doi: 10.1007/s10817-005-9018-6
    •
  • Bella, G., Massacci, F. and Paulson, LC., 2005. An Overview of the Verification of SET International Journal of Information Security, v. 4
    Doi: 10.1007/s10207-004-0047-7
    •
  • Ehmety, SO. and Paulson, LC., 2005. Mechanizing compositional reasoning for concurrent systems: some lessons FORM ASP COMPUT, v. 17
    Doi: 10.1007/s00165-004-0053-6
    •
  • Paulson, LC., 2005. Welcome defects as a sign of innovation? [1] Communications of the ACM, v. 48
    Doi: 10.1145/1096000.1096016
    •
  • Paulson, LC., 2004. Organizing Numerical Theories Using Axiomatic Type Classes Journal of Automated Reasoning, v. 33
    •
  • Paulson, LC., 2003. The Relative Consistency of the Axiom of Choice — Mechanized Using Isabelle/ZF LMS Journal of Computation and Mathematics, v. 6
    •
  • Bella, G., Massacci, F. and Paulson, LC., 2003. Verifying the SET registration protocols IEEE J SEL AREA COMM, v. 21
    Doi: 10.1109/JSAC.2002.806133
    •
  • Nipkow, T., Paulson, LC. and Wenzel, M., 2002. The basics LECT NOTES COMPUT SC, v. 2283
    •
  • Paulson, LC., 2001. Relations Between Secrets: Two Formal Analyses of the Yahalom Protocol. J. Comput. Secur., v. 9
    •
  • Paulson, LC., 2001. Mechanizing a Theory of Program Composition for UNITY ACM Transactions on Programming Languages and Systems, v. 25
    •
  • Paulson, LC., 2001. Keep E-journals affordable COMMUNICATIONS OF THE ACM, v. 44
    •
  • Paulson, LC., 2001. A Simple Formalization and Proof for the Mutilated Chess Board Logic Journal of the IGPL, v. 9
    Doi: 10.1093/jigpal/9.3.475
    •
  • Paulson, LC., 2001. Mechanizing a theory of program composition for UNITY ACM T PROGR LANG SYS, v. 23
    •
  • Fleuriot, JD. and Paulson, LC., 2000. Mechanizing Nonstandard Real Analysis LMS Journal of Computation and Mathematics, v. 3
    •
  • Paulson, LC., 2000. Mechanizing UNITY in Isabelle. ACM Trans. Comput. Log., v. 1
    Doi: 10.1145/343369.343370
    •
  • Roe, M., Lee, S., Christianson, B., Anderson, R., Wheeler, D., Blaze, M., Gollman, D., Gligor, V., Mao, WB., Paulson, L. and Kuhn, M., 2000. Performance of protocols (Transcript of discussion) SECURITY PROTOCOLS, v. 1796
    •
  • Bergadano, F., Morris, B., Roe, M., Lomas, M., Blaze, M., Lee, S., Christianson, B. and Paulson, L., 2000. Issues in multicast security SECURITY PROTOCOLS, v. 1796
    •
  • Kammüller, F. and Paulson, LC., 1999. A Formal Proof of Sylow’s theorem: An Experiment in Abstract Algebra with Isabelle HOL Journal of Automated Reasoning, v. 23
    Doi: 10.1023/A:1006269330992
    •
  • Lamport, L. and Paulson, LC., 1999. Should Your Specification Language Be Typed? ACM Transactions on Programming Languages and Systems, v. 21
    •
  • Paulson, LC., 1999. Final coalgebras as greatest fixed points in ZF set theory. Math. Struct. Comput. Sci., v. 9
    •
  • Paulson, LC., 1999. Inductive Analysis of the Internet Protocol TLS. ACM Trans. Inf. Syst. Secur., v. 2
    Doi: 10.1145/322510.322530
    •
  • Kammuller, F. and Paulson, LC., 1999. A formal proof of Sylow's theorem - An experiment in abstract algebra with Isabelle HOL J AUTOM REASONING, v. 23
    •
  • Paulson, LC., 1999. A Generic Tableau Prover and its Integration with Isabelle Journal of Universal Computer Science, v. 5
    •
  • Ballarin, C. and Paulson, LC., 1999. A Pragmatic Approach to Extending Provers by Computer Algebra - with Applications to Coding Theory. Fundam. Informaticae, v. 39
    Doi: 10.3233/FI-1999-391201
    •
  • Paulson, LC., 1998. The Inductive Approach to Verifying Cryptographic Protocols. J. Comput. Secur., v. 6
    •
  • Paulson, LC., 1997. Mechanizing coinduction and corecursion in higher-order logic J LOGIC COMPUT, v. 7
    •
  • Paulson, L., 1997. Cobol in question COMMUNICATIONS OF THE ACM, v. 40
    •
  • Paulson, LC. and Grabczewski, K., 1996. Mechanizing Set Theory. J. Autom. Reason., v. 17
    •
  • Paulson, LC. and cabczewski, KG., 1996. Mechanizing Set Theory: Cardinal Arithmetic and the Axiom of Choice Journal of Automated Reasoning, v. 17
    •
  • Paulson, LC., 1995. Set Theory for Verification: II. Induction and Recursion Journal of Automated Reasoning, v. 15
    •
  • PAULSON, LC., 1995. SET-THEORY FOR VERIFICATION .2. INDUCTION AND RECURSION J AUTOM REASONING, v. 15
    •
  • Paulson, LC., 1995. A Concrete Final Coalgebra Theorem for ZF Set Theory. CoRR, v. abs/cs/9511103
    •
  • PAULSON, LC., 1993. SET-THEORY FOR VERIFICATION .1. FROM FOUNDATIONS TO FUNCTIONS J AUTOM REASONING, v. 11
    •
  • Paulson, LC., 1993. Set Theory for Verification: I. From Foundations to Functions Journal of Automated Reasoning, v. 11
    •
  • NIPKOW, T. and PAULSON, LC., 1992. ISABELLE-91 LECT NOTES ARTIF INT, v. 607
    •
  • PAULSON, LC., 1990. A FORMULATION OF THE SIMPLE THEORY OF TYPES (FOR ISABELLE) LECT NOTES COMPUT SC, v. 417
    •
  • Paulson, LC., 1989. The Foundation of a Generic Theorem Prover. J. Autom. Reason., v. 5
    Doi: 10.1007/BF00248324
    •
  • Paulson, LC., 1989. The Foundation of a Generic Theorem Prover Journal of Automated Reasoning, v. 5
    •
  • PAULSON, L., COHEN, A. and GORDON, M., 1989. PROGRAM VERIFICATION - THE VERY IDEA COMMUNICATIONS OF THE ACM, v. 32
    •
  • PAULSON, LC., 1988. ISABELLE - THE NEXT 700 THEOREM PROVERS LECT NOTES COMPUT SC, v. 310
    •
  • Paulson, LC., 1987. Logic and Computation
    Doi: 10.1017/cbo9780511526602
    •
  • Paulson, LC., 1986. Proving Termination of Normalization Functions for Conditional Experessions. J. Autom. Reason., v. 2
    Doi: 10.1007/BF00246023
    •
  • Paulson, LC., 1986. Proving Termination of Normalization Functions for Conditional Expressions Journal of Automated Reasoning, v. 2
    Doi: 10.1007/BF00246023
    •
  • Paulson, LC., 1986. Natural Deduction as Higher-order Resolution Journal of Logic Programming, v. 3
    •
  • Paulson, LC., 1986. Constructing Recursion Operators in Intuitionistic Type Theory. J. Symb. Comput., v. 2
    Doi: 10.1016/S0747-7171(86)80002-5
    •
  • PAULSON, LC., 1986. CONSTRUCTING RECURSION OPERATORS IN INTUITIONISTIC TYPE THEORY J SYMB COMPUT, v. 2
    •
  • Paulson, LC., 1985. Verifying the Unification Algorithm in LCF Science of Computer Programming, v. 5
    •
  • Paulson, LC., 1985. Lessons learned from LCF: a Survey of Natural Deduction Proofs Computer Journal, v. 28
    •
  • Paulson, LC., 1983. A Higher-Order Implementation of Rewriting Science of Computer Programming, v. 3
    •
  • Macfarlane, A., 1896. QUATERNIONS. Science, v. 3
    Doi: 10.1126/science.3.55.99
    •

    Book chapters

  • Paulson, LC., 2023. Large-Scale Formal Proof for the Working Mathematician—Lessons Learnt from the ALEXANDRIA Project
    Doi: 10.1007/978-3-031-42753-4_1
    •
  • Paulson, LC., 2022. Wetzel: Formalisation of an Undecidable Problem Linked to the Continuum Hypothesis
    Doi: 10.1007/978-3-031-16681-5_6
    •
  • Abdulaziz, M. and Paulson, LC., 2018 (Accepted for publication). An Isabelle/HOL Formalisation of Green’s Theorem
    Doi: 10.1007/978-3-319-43144-4_1
    •
  • Passmore, G., Paulson, L. and de Moura, L., 2012. Real Algebraic Strategies for MetiTarski Proofs
    Doi: 10.1007/978-3-642-31374-5_24
    •
  • Paulson, LC., 2010. Functional Programming in ML.
  • Wenzel, M., Paulson, LC. and Nipkow, T., 2008. The Isabelle Framework
    Doi: 10.1007/978-3-540-71067-7_7
    •
  • Paulson, LC., 2001. Making Sense of Specifications: The Formalization of SET
    Doi: 10.1007/3-540-44810-1_12
    •
  • Paulson, LC., 2000. A fixedpoint approach to (co)inductive and (co)datatype definitions.
  • Paulson, LC., 1997. Generic Automatic Proof Tools
  • Paulson, LC., 1997. Tool Support for Logics of Programs
  • Paulson, LC., 1992. Designing a Theorem Prover
  • Paulson, LC., 1990. Isabelle: The Next 700 Theorem Provers

    • Internet publications

  • Paulson, LC., 2018 (No publication date). Home Page

    • Software

  • Gordon, MJC. and Paulson, LC., 2017. HOL88 proof assistant
    Doi: 10.17863/CAM.10246
    •
  • Paulson, LC., 2016. Isabelle-89 - source code from the interactive theorem prover Isabelle upon its release in 1989
    Doi: 10.17863/CAM.9037
    •
  • Paulson, LC., 2016. Isabelle-86 - source code from the interactive theorem prover Isabelle upon its original release in 1986
    Doi: 10.17863/CAM.9039
    •

    Datasets

  • Paulson, LC., 2016 (No publication date). Research data supporting "A semantics-directed compiler generator"

    • Books

  • 2010. Interactive Theorem Proving
    Doi: 10.1007/978-3-642-14052-5
    •
  • Kaufmann, M. and Paulson, L., 2010. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics): Preface
  • Paulson, LC., 1996. ML for the Working Programmer
  • Paulson, LC., 1994. Isabelle: A Generic Theorem Prover
  • Paulson, LC., 1991. ML for the Working Programmer
  • Paulson, LC., 1987. Logic and Computation: Interactive proof with Cambridge LCF

    • Reports

  • Paulson, LC., 1997. Mechanized Proofs of Security Protocols: Needham-Schroeder with Public Keys
  • Paulson, LC., 1996. A Simple Formalization and Proof for the Mutilated Chess Board
  • Paulson, LC., 1993. Introduction to Isabelle
  • Paulson, LC., 1993. The Isabelle Reference Manual
  • Paulson, LC., 1993. Isabelle’s Object-Logics
  • Paulson, LC., 1993. A Fixedpoint Approach to Implementing (Co)Inductive Definitions
  • Paulson, LC., 1992. Set Theory as a Computational Logic: I. From Foundations to Functions
  • Paulson, LC. and Nipkow, T., 1990. Isabelle Tutorial and User’s Manual
  • Paulson, LC., 1988. A preliminary user’s manual for Isabelle

    • Theses / dissertations

  • Paulson, LC., 1981. A Compiler Generator for Semantic Grammars
    • Conference proceedings

    2024

  • Edmonds, C. and Paulson, LC., 2024. Formal Probabilistic Methods for Combinatorial Structures using the Lovász Local Lemma Cpp 2024 Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs Co Located with Popl 2024,
    Doi: 10.1145/3636501.3636946
    •
  • Eberl, M., Bordg, A., Paulson, LC. and Li, W., 2024. Formalising Half of a Graduate Textbook on Number Theory Leibniz International Proceedings in Informatics Lipics, v. 309
    Doi: 10.4230/LIPIcs.ITP.2024.40
    •

    2022

  • Mangla, C., Holden, SB. and Paulson, LC., 2022. Bayesian Ranking for Strategy Scheduling in Automated Theorem Provers Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, v. 13385 LNAI
    Doi: 10.1007/978-3-031-10769-6_33
    •
  • Paulson, LC., 2022. Wetzel: Formalisation of an Undecidable Problem Linked to the Continuum Hypothesis. CICM, v. 13467
    •
  • Edmonds, C. and Paulson, LC., 2022. Formalising Fisher's Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics 13th International Conference on Interactive Theorem Proving (2022). 11:1-11:19,
    •
  • Edmonds, C. and Paulson, LC., 2022. Formalising Fisher's Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics Leibniz International Proceedings in Informatics Lipics, v. 237
    Doi: 10.4230/LIPIcs.ITP.2022.11
    •

    2021

  • Li, W., Yu, L., Wu, Y. and Paulson, LC., 2021. ISARSTEP: A BENCHMARK FOR HIGH-LEVEL MATHEMATICAL REASONING Iclr 2021 9th International Conference on Learning Representations,
    •
  • Edmonds, C. and Paulson, LC., 2021. A Modular First Formalisation of Combinatorial Design Theory. CICM, v. 12833
    •
  • Edmonds, C. and Paulson, LC., 2021. A Modular First Formalisation of Combinatorial Design Theory Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, v. 12833 LNAI
    Doi: 10.1007/978-3-030-81097-9_1
    •

    2020 (No publication date)

  • Słowik, A., Mangla, C., Jamnik, M., Holden, S. and Paulson, L., 2020 (No publication date). Bayesian Optimisation for Heuristic Configuration in Automated Theorem Proving EPiC Series in Computing, v. 71
    Doi: 10.29007/q91g
    •

    2020 (Accepted for publication)

  • de Vilhena, PE. and Paulson, L., 2020 (Accepted for publication). Algebraically Closed Fields in Isabelle/HOL Automated Reasoning—10th International Joint Conference, IJCAR 2020,
    Doi: 10.1007/978-3-030-51054-1_12
    •

    2020

  • Mangla, C., Holden, SB. and Paulson, LC., 2020. Bayesian optimisation of solver parameters in CBMC Ceur Workshop Proceedings, v. 2854
    •
  • 2020. Automated Reasoning
    Doi: 10.1007/978-3-030-51074-9
    •
  • Słowik, A., Mangla, C., Jamnik, M., Holden, SB. and Paulson, LC., 2020. Bayesian optimisation for premise selection in automated theorem proving (student abstract) Aaai 2020 34th Aaai Conference on Artificial Intelligence,
    •
  • Slowik, A., Mangla, C., Jamnik, M., Holden, SB. and Paulson, LC., 2020. Bayesian Optimisation for Premise Selection in Automated Theorem Proving (Student Abstract). Proceedings of the AAAI Conference on Artificial Intelligence, 34(10), v. 34
    Doi: 10.1609/aaai.v34i10.7232
    •

    2019

  • Li, W. and Paulson, LC., 2019. Counting polynomial roots in Isabelle/HOL: A formal proof of the Budan-Fourier theorem Cpp 2019 Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs Co Located with Popl 2019,
    Doi: 10.1145/3293880.3294092
    •

    2018 (Accepted for publication)

  • Li, W. and Paulson, LC., 2018 (Accepted for publication). Counting Polynomial Roots in Isabelle/HOL: A Formal Proof of the Budan-Fourier Theorem Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs,
    Doi: 10.1145/3293880.3294092
    •

    2017

  • Huang, Z., England, M., Davenport, JH. and Paulson, LC., 2017. Using machine learning to decide when to precondition cylindrical algebraic decomposition with groebner bases Proceedings - 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2016,
    Doi: 10.1109/SYNASC.2016.020
    •
  • Paulson, LC., 2017. Porting the HOL Light Analysis Library: Some Lessons (Invited Talk) PROCEEDINGS OF THE 6TH ACM SIGPLAN CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP'17,
    Doi: 10.1145/3018610.3023366
    •

    2016

  • Li, W. and Paulson, LC., 2016. A modular, efficient formalisation of real algebraic numbers Cpp 2016 Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs Co Located with Popl 2016,
    Doi: 10.1145/2854065.2854074
    •
  • Huang, Z., England, M., Davenport, JH. and Paulson, LC., 2016. Using Machine Learning to Decide When to Precondition Cylindrical Algebraic Decomposition With Groebner Bases PROCEEDINGS OF 2016 18TH INTERNATIONAL SYMPOSIUM ON SYMBOLIC AND NUMERIC ALGORITHMS FOR SCIENTIFIC COMPUTING (SYNASC),
    Doi: 10.1109/SYNASC.2016.14
    •

    2015

  • Huang, Z., England, M., Wilson, D., Davenport, JH. and Paulson, LC., 2015. A comparison of three heuristics to choose the variable ordering for cylindrical algebraic decomposition ACM Communications in Computer Algebra, v. 48
    Doi: 10.1145/2733693.2733706
    •
  • Sultana, N., Benzmüller, C. and Paulson, LC., 2015. Proofs and reconstructions Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, v. 9322
    Doi: 10.1007/978-3-319-24246-0_16
    •
  • Paulson, LC., 2015. A formalisation of finite automata using hereditarily finite sets Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, v. 9195
    Doi: 10.1007/978-3-319-21401-6_15
    •

    2014

  • Jackson, P., Sogokon, A., Bridge, J. and Paulson, L., 2014. Verifying hybrid systems involving transcendental functions Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, v. 8430 LNCS
    Doi: 10.1007/978-3-319-06200-6_14
    •

    2013

  • Paulson, LC., 2013. MetiTarski's Menagerie of Cooperating Systems. FroCos, v. 8152
    •

    2012

  • Paulson, LC., 2012. MetiTarski: Past and Future. ITP, v. 7406
    •

    2010 (No publication date)

  • Paulson, LC. and Susanto, KW., 2010 (No publication date). Source-Level Proof Reconstruction for Interactive Theorem Proving
  • Meng, J. and Paulson, LC., 2010 (No publication date). Translating Higher-Order Problems to First-Order Clauses
  • Meng, J. and Paulson, LC., 2010 (No publication date). Lightweight Relevance Filtering for Machine-Generated Resolution Problems

    • 2010

  • Paulson, LC., 2010. Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem Provers. PAAR@IJCAR, v. 9
    •
  • Narayanan, R., Akbarpour, B., Zaki, MH., Tahar, S. and Paulson, LC., 2010. Formal verification of analog circuits in the presence of noise and process variation. DATE,
    •
  • 2010. Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings ITP, v. 6172
    •
  • Paulson, LC. and Blanchette, JC., 2010. Three years of experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers. IWIL@LPAR, v. 2
    •

    2009

  • Akbarpour, B. and Paulson, LC., 2009. Applications of MetiTarski in the Verification of Control and Hybrid Systems HYBRID SYSTEMS: COMPUTATION AND CONTROL, v. 5469
    •
  • Akbarpour, B. and Paulson, LC., 2009. Applications of MetiTarski in the Verification of Control and Hybrid Systems Hybrid Systems: Computation and Control,
    •
  • Denman, W., Akbarpour, B., Tahar, S., Zaki, M. and Paulson, LC., 2009. Formal Verification of Analog Designs using MetiTarski Formal Methods in Computer Aided Design,
    Doi: 10.1109/FMCAD.2009.5351136
    •
  • Benzmüller, C. and Paulson, LC., 2009. Quantified Multimodal Logics in Simple Type Theory CoRR, v. abs/0905.2435
    •
  • Akbarpour, B. and Paulson, LC., 2009. Applications of MetiTarski in the Verification of Control and Hybrid Systems. HSCC, v. 5469
    •

    2008

  • Wenzel, M., Paulson, LC. and Nipkow, T., 2008. The Isabelle Framework Theorem Proving in Higher Order Logics: TPHOLs 2008,
    Doi: 10.1007/978-3-540-71067-7_7
    •
  • Benzmüller, C., Paulson, LC., Theiss, F. and Fietzke, A., 2008. LEO-II - A Cooperative Automatic Theorem Prover for Higher-Order Logic Automated Reasoning — 4th International Joint Conference, IJCAR 2008,
    Doi: 10.1007/978-3-540-71070-7_14
    •
  • Paulson, LC., 2008. The relative consistency of the axiom of choice - Mechanized using Isabelle/ZF LOGIC AND THEORY OF ALGORITHMS, v. 5028
    •

    2007

  • Meng, J., Paulson, LC. and Klein, G., 2007. A Termination Checker for Isabelle Hoare Logic 4th International Verification Workshop - VERIFY’07, v. 259
    •
  • Akbarpour, B. and Paulson, L., 2007. Extending a Resolution Prover for Inequalities on Elementary Functions Logic for Programming, Artificial Intelligence, and Reasoning,
    Doi: 10.1007/978-3-540-75560-9_6
    •

    2006

  • Wenzel, M. and Paulson, LC., 2006. Isabelle/Isar.
  • Akbarpour, B. and Paulson, LC., 2006. Towards Automatic Proofs of Inequalities Involving Elementary Functions PDPAR: Pragmatics of Decision Procedures in Automated Reasoning,
    •
  • 2006. FLoC’06 Workshop on Empirically Successful Computerized Reasoning

    • 2005

  • Bella, G., Longo, C. and Paulson, LC., 2005. Is the verification problem for cryptographic protocols solved? SECURITY PROTOCOLS, v. 3364
    •
  • Nipkow, T. and Paulson, LC., 2005. Proof Pearl: Defining Functions Over Finite Sets Theorem Proving in Higher Order Logics: TPHOLs 2005,
    Doi: 10.1007/11541868_25
    •
  • Nipkow, T. and Paulson, LC., 2005. Proof pearl: Defining functions over finite sets THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS, v. 3603
    •

    2004

  • Meng, J. and Paulson, LC., 2004. Experiments on supporting interactive proof using resolution AUTOMATED REASONING, PROCEEDINGS, v. 3097
    •
  • Meng, J. and Paulson, LC., 2004. Experiments On Supporting Interactive Proof Using Resolution Automated Reasoning — Second International Joint Conference, IJCAR 2004,
    Doi: 10.1007/b98691
    •
  • Paulson, LC., 2004. The descent of BAN COMPUTER SYSTEMS: THEORY, TECHNOLOGY AND APPLICATIONS,
    •
  • Bella, G. and Paulson, LC., 2004. Analyzing delegation properties SECURITY PROTOCOLS, v. 2845
    •

    2003

  • Paulson, LC., 2003. Verifying the SET protocol: Overview FORMAL ASPECTS OF SECURITY, v. 2629
    •
  • Bella, G., Longo, C. and Paulson, LC., 2003. Verifying Second-Level Security Protocols Theorem Proving in Higher Order Logics: TPHOLs 2003,
    •

    2002

  • Bella, G. and Paulson, LC., 2002. A proof of non-repudiation SECURITY PROTOCOLS, v. 2467
    •
  • Paulson, L., 2002. A proof of non-repudiation - (Transcript of discussion) SECURITY PROTOCOLS, v. 2467
    •
  • Bella, G., Paulson, LC. and Massacci, F., 2002. The verification of an industrial payment protocol: the SET purchase phase. CCS,
    •
  • Christianson, B., Aura, T., Wheeler, D., Harbison, W., Gligor, V., Paulson, L., Blaze, M. and Ioannidis, J., 2002. Concluding discussion - When does confidentiality harm security? SECURITY PROTOCOLS, v. 2467
    •
  • Paulson, LC., 2002. The Reflection Theorem: A Study in Meta-theoretic Reasoning. CADE, v. 2392
    •
  • Ehmety, SO. and Paulson, LC., 2002. Program Composition in Isabelle/UNITY Workshop on Formal Methods for Parallel Programming: Theory and Applications; text on CD-ROM,
    •

    2001

  • Paulson, LC., 2001. SET Cardholder Registration: The Secrecy Proofs. IJCAR, v. 2083
    •
  • Bella, G. and Paulson, LC., 2001. Mechanical Proofs about a Non-repudiation Protocol. TPHOLs, v. 2152
    •
  • Bella, G., Massacci, F., Paulson, LC. and Tramontano, P., 2001. Making sense of specifications: The formalization of SET (Extended abstract) Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, v. 2133
    Doi: 10.1007/3-540-44810-1_11
    •

    2000

  • Paulson, LC., 2000. Making Sense of Specifications: The Formalization of SET (Transcript of Discussion). Security Protocols Workshop, v. 2133
    •
  • Paulson, LC., 2000. The Yahalom protocol SECURITY PROTOCOLS, v. 1796
    •
  • Paulson, LC., 2000. Relations between secrets: The Yahalom protocol SECURITY PROTOCOLS, v. 1796
    •
  • Bella, G., Massacci, F., Paulson, LC. and Tramontano, P., 2000. Formal verification of Cardholder Registration in SET COMPUTER SECURITY - ESORICS 2000, PROCEEDINGS, v. 1895
    •
  • Bella, G., Massacci, F., Paulson, LC. and Tramontano, P., 2000. Formal Verification of Cardholder Registration in SET Computer Security — ESORICS 2000,
    •
  • Paulson, LC., 2000. Relations between secrets: The yahalom protocol extended abstract Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, v. 1796
    Doi: 10.1007/10720107_10
    •
  • Bella, G., Massacci, F., Paulson, LC. and Tramontano, P., 2000. Making Sense of Specifications: The Formalization of SET. Security Protocols Workshop, v. 2133
    •

    1999

  • Fleuriot, J. and Paulson, LC., 1999. Proving Newton’s Propositio Kepleriana Using Geometry and Nonstandard Analysis in Isabelle Workshop on Automated Deduction in Geometry, Second International Workshop, ADG’98,
    •
  • Kammüller, F., Wenzel, M. and Paulson, LC., 1999. Locales: A Sectioning Concept for Isabelle Theorem Proving in Higher Order Logics: TPHOLs ’99,
    •
  • Paulson, LC., 1999. Proving Security Protocols Correct. LICS,
    Doi: 10.1109/LICS.1999.782632
    •

    1998

  • Paulson, LC., 1998. Inductive Analysis of the Internet Protocol TLS (Position Paper). Security Protocols Workshop, v. 1550
    •
  • Paulson, LC., 1998. Inductive Analysis of the Internet Protocol TLS (Transcript of Discussion). Security Protocols Workshop, v. 1550
    •
  • Paulson, LC., 1998. A Generic Tableau Prover and its Integration with Isabelle (Extended Abstract) CADE-15 Workshop on Integration of Deduction Systems,
    •
  • Bella, G. and Paulson, LC., 1998. Kerberos Version IV: Inductive Analysis of the Secrecy Goals Computer Security — ESORICS 98,
    •
  • Ballarin, C. and Paulson, LC., 1998. Reasoning About Coding Theory: The Benefits We Get from Computer Algebra. AISC, v. 1476
    •
  • Ballarin, C. and Paulson, LC., 1998. Reasoning about coding theory: The benefits we get from computer algebra Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), v. 1476
    •
  • Bella, G. and Paulson, LC., 1998. Mechanising BAN Kerberos by the Inductive Method Computer Aided Verification: 10th International Conference, CAV ’98,
    •
  • Fleuriot, J. and Paulson, LC., 1998. A Combination of Nonstandard Analysis and Geometry Theorem Proving, with Application to Newton’s Principia Automated Deduction — CADE-15 International Conference,
    •
  • Paulson, L., 1998. Inductive analysis of the internet protocol TLS Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, v. 1550
    Doi: 10.1007/3-540-49135-X_2
    •

    1997

  • Bella, G. and Paulson, LC., 1997. Using Isabelle to Prove Properties of the Kerberos Authentication System Workshop on Design and Formal Verification of Security Protocols,
    •
  • Paulson, LC., 1997. Mechanizing Coinduction and Corecursion in Higher-Order Logic. J. Log. Comput., v. 7
    Doi: 10.1093/logcom/7.2.175
    •
  • Paulson, LC., 1997. Proving Properties of Security Protocols by Induction 10th Computer Security Foundations Workshop,
    •
  • Paulson, LC., 1997. Mechanized Proofs for a Recursive Authentication Protocol 10th Computer Security Foundations Workshop,
    •

    1995

  • 1995. First Isabelle Users Workshop

    • 1994

  • Paulson, LC., 1994. A Fixedpoint Approach to Implementing (Co)Inductive Definitions Automated Deduction — CADE-12,
    •
  • Paulson, LC., 1994. A Concrete Final Coalgebra Theorem for ZF Set Theory. TYPES, v. 996
    •

    1993

  • Paulson, LC., 1993. A Formulation of the Simple Theory of Types (for Isabelle) CoRR, v. cs.LO/9301107
    •

    1992

  • NIPKOW, T. and PAULSON, LC., 1992. ISABELLE-91 AUTOMATED DEDUCTION - CADE-11, v. 607
    •
  • Nipkow, T. and Paulson, LC., 1992. Isabelle-91 (system abstract) Automated Deduction — CADE-11,
    •

    1991

  • Paulson, LC. and Smith, AW., 1991. Logic Programming, Functional Programming, and Inductive Definitions Extensions of Logic Programming,
    •

    1990

  • Paulson, LC., 1990. A Formulation of the Simple Theory of Types (for Isabelle) COLOG-88: International Conference on Computer Logic,
    •

    1989

  • Paulson, LC. and Smith, AW., 1989. Logic Programming, Functional Programming, and Inductive Definitions. ELP, v. 475
    •

    1988

  • Paulson, LC., 1988. Isabelle: The Next Seven Hundred Theorem Provers. CADE, v. 310
    •

    1987

  • Paulson, LC., 1987. NEXT SEVEN HUNDRED THEOREM PROVERS. IEE Colloquium Digest,
    •

    1986

  • Paulson, LC., 1986. Natural Deduction as Higher-Order Resolution. J. Log. Program., v. 3
    Doi: 10.1016/0743-1066(86)90015-4
    •

    1985

  • Paulson, LC., 1985. Verifying the Unification Algorithm in LCF. Sci. Comput. Program., v. 5
    Doi: 10.1016/0167-6423(85)90009-7
    •

    1984

  • Paulson, LC., 1984. Deriving Structural Induction in LCF. Semantics of Data Types, v. 173
    •

    1983

  • Paulson, LC., 1983. Compiler Generation from Denotational Semantics. Method and tools for compiler construction,
    •
  • Paulson, LC., 1983. A Higher-Order Implementation of Rewriting. Sci. Comput. Program., v. 3
    Doi: 10.1016/0167-6423(83)90008-4
    •

    1982

  • Paulson, L., 1982. A Semantics-Directed Compiler Generator Ninth Annual ACM Symposium on Principles of Programming Languages,
    •
  • Paulson, LC., 1982. A Semantics-Directed Compiler Generator. POPL,
    •
    Book chapters

    2023

  • Paulson, LC., 2023. Large-Scale Formal Proof for the Working Mathematician—Lessons Learnt from the ALEXANDRIA Project
    Doi: 10.1007/978-3-031-42753-4_1
    •

    2022

  • Paulson, LC., 2022. Wetzel: Formalisation of an Undecidable Problem Linked to the Continuum Hypothesis
    Doi: 10.1007/978-3-031-16681-5_6
    •

    2018 (Accepted for publication)

  • Abdulaziz, M. and Paulson, LC., 2018 (Accepted for publication). An Isabelle/HOL Formalisation of Green’s Theorem
    Doi: 10.1007/978-3-319-43144-4_1
    •

    2012

  • Passmore, G., Paulson, L. and de Moura, L., 2012. Real Algebraic Strategies for MetiTarski Proofs
    Doi: 10.1007/978-3-642-31374-5_24
    •

    2010

  • Paulson, LC., 2010. Functional Programming in ML.

    • 2008

  • Wenzel, M., Paulson, LC. and Nipkow, T., 2008. The Isabelle Framework
    Doi: 10.1007/978-3-540-71067-7_7
    •

    2001

  • Paulson, LC., 2001. Making Sense of Specifications: The Formalization of SET
    Doi: 10.1007/3-540-44810-1_12
    •

    2000

  • Paulson, LC., 2000. A fixedpoint approach to (co)inductive and (co)datatype definitions.

    • 1997

  • Paulson, LC., 1997. Generic Automatic Proof Tools
  • Paulson, LC., 1997. Tool Support for Logics of Programs

    • 1992

  • Paulson, LC., 1992. Designing a Theorem Prover

    • 1990

  • Paulson, LC., 1990. Isabelle: The Next 700 Theorem Provers
    • Journal articles

    2023

  • Edmonds, C., Koutsoukou-Argyraki, A. and Paulson, LC., 2023. Formalising Szemerédi’s Regularity Lemma and Roth’s Theorem on Arithmetic Progressions in Isabelle/HOL Journal of Automated Reasoning, v. 67
    Doi: 10.1007/s10817-022-09650-2
    •

    2022 (Accepted for publication)

  • Paulson, LC., 2022 (Accepted for publication). A Formalised Theorem in the Partition Calculus Annals of Pure and Applied Logic,
    •
  • Bordg, A., Paulson, L. and Li, W., 2022 (Accepted for publication). Simple Type Theory is not too Simple: Grothendieck’s Schemes Without Dependent Types Experimental Mathematics, v. 31
    Doi: 10.1080/10586458.2022.2062073
    •

    2022

  • Coward, S., Paulson, L., Drane, T. and Morini, E., 2022. Formal Verification of Transcendental Fixed- and Floating-point Algorithms using an Automatic Theorem Prover Formal Aspects of Computing, v. 34
    Doi: 10.1145/3543670
    •
  • Bayer, J., Benzmüller, C., Buzzard, K., David, M., Lamport, L., Matiyasevich, Y., Paulson, L., Schleicher, D., Stock, B. and Zelmanov, E., 2022. Mathematical Proof Between Generations Notices of the American Mathematical Society, v. 71
    •

    2021 (Accepted for publication)

  • Paulson, LC., 2021 (Accepted for publication). Ackermann's Function in Iterative Form: A Proof Assistant Experiment Bulletin of Symbolic Logic,
    •
  • Koutsoukou-Argyraki, A., Li, W. and Paulson, LC., 2021 (Accepted for publication). Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL Experimental Mathematics,
    •
  • Džamonja, M., Koutsoukou-Argyraki, A. and Paulson, LC., 2021 (Accepted for publication). Formalising Ordinal Partition Relations Using Isabelle/HOL Experimental Mathematics,
    •

    2021

  • Paulson, LC., 2021. The Inductive Approach to Verifying Cryptographic Protocols. CoRR, v. abs/2105.06319
    •
  • Bordg, A., Paulson, LC. and Li, W., 2021. Grothendieck's Schemes in Algebraic Geometry. Arch. Formal Proofs, v. 2021
    •

    2020

  • Paulson, LC., 2020. Ordinal Partitions. Arch. Formal Proofs, v. 2020
    •
  • Li, W. and Paulson, LC., 2020. Evaluating Winding Numbers and Counting Complex Roots Through Cauchy Indices in Isabelle/HOL. J. Autom. Reasoning, v. 64
    Doi: 10.1007/s10817-019-09521-3
    •
  • Paulson, LC., 2020. The Nash-Williams Partition Theorem. Arch. Formal Proofs, v. 2020
    •
  • Li, W., Yu, L., Wu, Y. and Paulson, LC., 2020. Modelling High-Level Mathematical Reasoning in Mechanised Declarative Proofs. CoRR, v. abs/2006.09265
    •

    2019 (Accepted for publication)

  • Huang, Z., England, M., Wilson, D., Davenport, JH. and Paulson, LC., 2019 (Accepted for publication). Using Machine Learning to Improve Cylindrical Algebraic Decomposition Mathematics in Computer Science,
    Doi: 10.1007/s11786-019-00394-8
    •

    2019

  • Paulson, LC., Nipkow, T. and Wenzel, M., 2019. From LCF to Isabelle/HOL Formal Aspects of Computing, v. 31
    Doi: 10.1007/s00165-019-00492-1
    •
  • Paulson, LC., 2019. Formalising Mathematics in Simple Type Theory
    Doi: 10.1007/978-3-030-15655-8_20
    •
  • Słowik, A., Mangla, C., Jamnik, M., Holden, SB. and Paulson, LC., 2019. Bayesian Optimisation with Gaussian Processes for Premise Selection
  • Li, W., Passmore, GO. and Paulson, LC., 2019. Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle/HOL JOURNAL OF AUTOMATED REASONING, v. 62
    Doi: 10.1007/s10817-017-9424-6
    •
  • Paulson, LC., 2019. Zermelo Fraenkel Set Theory in Higher-Order Logic. Arch. Formal Proofs, v. 2019
    •
  • Huang, Z., England, M., Wilson, DJ., Bridge, JP., Davenport, JH. and Paulson, LC., 2019. Using Machine Learning to Improve Cylindrical Algebraic Decomposition. Math. Comput. Sci., v. 13
    •
  • Paulson, LC., 2019. Fourier Series. Arch. Formal Proofs, v. 2019
    •
  • Paulson, L., Nipkow, T. and Wenzel, M., 2019. From LCF to Isabelle/HOL Formal Aspects of Computing, v. 31
    Doi: 10.1007/s00165-019-00492-1
    •
  • Abdulaziz, M. and Paulson, LC., 2019. An Isabelle/HOL Formalisation of Green’s Theorem Journal of Automated Reasoning, v. 63
    Doi: 10.1007/s10817-018-9495-z
    •

    2018 (Accepted for publication)

  • Paulson, LC., 2018 (Accepted for publication). Computational Logic: Its Origins and Applications Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences,
    •

    2018

  • Avigad, J., Blanchette, JC., Klein, G., Paulson, L., Popescu, A. and Snelting, G., 2018. Introduction to Milestones in Interactive Theorem Proving Journal of Automated Reasoning, v. 61
    Doi: 10.1007/s10817-018-9465-5
    •
  • Paulson, LC., 2018. Michael John Caldwell Gordon (FRS 1994), 28 February 1948 -- 22 August 2017 Biographical memoirs of fellows of the Royal Society. Royal Society (Great Britain), v. 65
    Doi: 10.1098/rsbm.2018.0019
    •
  • Eberl, M. and Paulson, LC., 2018. The Prime Number Theorem. Arch. Formal Proofs, v. 2018
    •
  • Paulson, LC., 2018. Predicting Failure of the University COMMUNICATIONS OF THE ACM, v. 61
    •

    2017 (Accepted for publication)

  • Li, W., Passmore, G. and Paulson, LC., 2017 (Accepted for publication). Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle/HOL Journal of Automated Reasoning,
    Doi: 10.1007/s10817-017-9424-6
    •

    2017

  • Paulson, LC., 2017. Time to Retire 'Computational Thinking'? COMMUNICATIONS OF THE ACM, v. 60
    •

    2016

  • Paulson, LC., 2016. The Cartan Fixed Point Theorems. Arch. Formal Proofs, v. 2016
    •
  • Abdulaziz, M. and Paulson, LC., 2016. An Isabelle/HOL formalisation of Green’s theorem Lecture Notes in Computer Science, v. 9807
    Doi: 10.1007/978-3-319-43144-4_1
    •
  • Li, W. and Paulson, LC., 2016. A formal proof of Cauchy’s residue theorem Lecture Notes in Computer Science, v. 9807
    Doi: 10.1007/978-3-319-43144-4_15
    •
  • Blanchette, JC., Kaliszyk, C., Paulson, LC. and Urban, J., 2016. Hammering towards QED Journal of Formalized Reasoning, v. 9
    •
  • Hibon, Q. and Paulson, LC., 2016. Source Coding Theorem. Arch. Formal Proofs, v. 2016
    •

    2015

  • Paulson, LC., 2015. Finite Automata in Hereditarily Finite Set Theory. Arch. Formal Proofs, v. 2015
    •
  • Paulson, LC., 2015. A Mechanised Proof of Gödel’s Incompleteness Theorems Using Nominal Isabelle Journal of Automated Reasoning,
    Doi: 10.1007/s10817-015-9322-8
    •
  • Martina, JE. and Paulson, LC., 2015. Verifying multicast-based security protocols using the inductive method International Journal of Information Security, v. 14
    Doi: 10.1007/s10207-014-0251-z
    •
  • Paulson, LC., 2015. A Formalisation of Finite Automata using Hereditarily Finite Sets. CoRR, v. abs/1505.01662
    •
  • Paulson, LC., 2015. Abolish Software Warranty Disclaimers COMMUNICATIONS OF THE ACM, v. 58
    •
  • Benzmüller, C., Sultana, N., Paulson, LC. and Theiß, F., 2015. The Higher-Order Prover Leo-II. J Autom Reason, v. 55
    Doi: 10.1007/s10817-015-9348-y
    •
  • Paulson, LC., 2015. A Mechanised Proof of Gödel’s Incompleteness Theorems Using Nominal Isabelle Journal of Automated Reasoning, v. 55
    Doi: 10.1007/s10817-015-9322-8
    •

    2014

  • Paulson, LC., 2014. Provenance of British Computing COMMUNICATIONS OF THE ACM, v. 57
    •
  • Bridge, JP., Holden, SB. and Paulson, LC., 2014. Machine Learning for First-Order Theorem Proving Journal of Automated Reasoning,
    •
  • Paulson, LC., 2014. Theorem proving and the real numbers: Overview and challenges Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, v. 8430 LNCS
    •
  • Paulson, LC., 2014. Real-Valued Special Functions: Upper and Lower Bounds. Arch. Formal Proofs, v. 2014
    •
  • Bridge, JP., Holden, SB. and Paulson, LC., 2014. Machine learning for first-order theorem proving: Learning to select a good Heuristic Journal of Automated Reasoning, v. 53
    Doi: 10.1007/s10817-014-9301-5
    •
  • Huang, Z., England, M., Wilson, D., Davenport, JH., Paulson, LC. and Bridge, J., 2014. Applying machine learning to the problem of choosing a heuristic to select the variable ordering for cylindrical algebraic decomposition Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, v. 8543 LNAI
    Doi: 10.1007/978-3-319-08434-3_8
    •
  • PAULSON, LC., 2014. A MACHINE-ASSISTED PROOF OF GÖDEL'S INCOMPLETENESS THEOREMS FOR THE THEORY OF HEREDITARILY FINITE SETS Review of Symbolic Logic,
    Doi: 10.1017/S1755020314000112
    •
  • Paulson, LC., 2014. Automated theorem proving for special functions: The next phase Proceedings of the 2014 Symposium on Symbolic Numeric Computation Snc 2014,
    Doi: 10.1145/2631948.2631950
    •
  • Paulson, LC., 2014. A machine-assisted proof of Gödel's incompleteness theorems for the theory of hereditarily finite sets Review of Symbolic Logic, v. 7
    Doi: 10.1017/S1755020314000112
    •
  • Huang, Z., England, M., Wilson, DJ., Davenport, JH., Paulson, LC. and Bridge, JP., 2014. Applying machine learning to the problem of choosing a heuristic to select the variable ordering for cylindrical algebraic decomposition. CoRR, v. abs/1404.6369
    •
  • Huang, Z., England, M., Wilson, D., Davenport, JH. and Paulson, LC., 2014. A comparison of three heuristics to choose the variable ordering for CAD ACM Communications in Computer Algebra 48:3 (issue 189), pp. 121-123, ACM, 2014,
    •

    2013

  • Benzmüller, C. and Paulson, LC., 2013. Quantified Multimodal Logics in Simple Type Theory Logica Universalis, v. 7
    Doi: 10.1007/s11787-012-0052-y
    •
  • Martina, JE. and Paulson, LC., 2013. Verifying multicast-based security protocols using the inductive method Proceedings of the ACM Symposium on Applied Computing,
    Doi: 10.1145/2480362.2480703
    •
  • Paulson, LC., 2013. The Hereditarily Finite Sets. Arch. Formal Proofs, v. 2013
    •
  • Paulson, LC., 2013. Gödel's Incompleteness Theorems. Arch. Formal Proofs, v. 2013
    •
  • Bridge, JP. and Paulson, LC., 2013. Case splitting in an automatic theorem prover for real-valued special functions Journal of Automated Reasoning, v. 50
    Doi: 10.1007/s10817-012-9245-6
    •
  • Sultana, N., Blanchette, JC. and Paulson, LC., 2013. LEO-II and Satallax on the Sledgehammer test bench Journal of Applied Logic, v. 11
    Doi: 10.1016/j.jal.2012.12.002
    •
  • Paulson, LC., 2013. What we want from computer science Communications of the ACM, v. 56
    Doi: 10.1145/2483852.2483856
    •
  • Blanchette, JC., Böhme, S. and Paulson, LC., 2013. Extending sledgehammer with SMT solvers Journal of Automated Reasoning, v. 51
    Doi: 10.1007/s10817-013-9278-5
    •

    2012

  • Paulson, LC., 2012. What liability for faulty software? Communications of the ACM, v. 55
    Doi: 10.1145/2076450.2076452
    •
  • Romanos, R. and Paulson, LC., 2012. Proving the Impossibility of Trisecting an Angle and Doubling the Cube. Arch. Formal Proofs, v. 2012
    •

    2011

  • Blanchette, JC., Böhme, S. and Paulson, LC., 2011. Extending sledgehammer with SMT solvers Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, v. 6803 LNAI
    Doi: 10.1007/978-3-642-22438-6_11
    •

    2010

  • Paulson, LC., 2010. Robin Milner The Elegant Pragmatist (vol 53, pg 20, 2010) COMMUNICATIONS OF THE ACM, v. 53
    •
  • Benzmueller, C. and Paulson, LC., 2010. Multimodal and Intuitionistic Logics in Simple Type Theory Logic Jnl IGPL,
    Doi: 10.1093/jigpal/jzp080
    •
  • Akbarpour, B. and Paulson, LC., 2010. MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions J AUTOM REASONING, v. 44
    Doi: 10.1007/s10817-009-9149-2
    •

    2009

  • Paulson, LC., 2009. Refocus fragmented CS conference culture [3] Communications of the ACM, v. 52
    Doi: 10.1145/1536616.1536619
    •
  • Paulson, LC., 2009. Refocus Fragmented CS Conference Culture COMMUNICATIONS OF THE ACM, v. 52
    •
  • Akbarpour, B. and Paulson, LC., 2009. MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions Journal of Automated Reasoning,
    •
  • Meng, J. and Paulson, LC., 2009. Lightweight relevance filtering for machine-generated resolution problems J APPL LOGIC, v. 7
    Doi: 10.1016/j.jal.2007.07.004
    •

    2008

  • Meng, J. and Paulson, LC., 2008. Translating higher-order clauses to first-order clauses J AUTOM REASONING, v. 40
    Doi: 10.1007/s10817-007-9085-y
    •
  • Akbarpour, B. and Paulson, L., 2008. MetiTarski: An Automatic Prover for the Elementary Functions Intelligent Computer Mathematics,
    •
  • Nipkow, T. and Paulson, LC., 2008. Fun With Tilings. Arch. Formal Proofs, v. 2008
    •

    2007

  • Beckert, B. and Paulson, LC., 2007. Journal of Automated Reasoning: Preface Journal of Automated Reasoning, v. 38
    Doi: 10.1007/s10817-006-9058-6
    •
  • Beckert, B. and Paulson, LC., 2007. Special issue on automated reasoning with analytic tableaux - Preface J AUTOM REASONING, v. 38
    Doi: 10.1007/s10817-006-9058-6
    •
  • Paulson, LC., 2007. Even a good abstraction needs experience and testing, too COMMUNICATIONS OF THE ACM, v. 50
    •

    2006

  • Bella, G. and Paulson, LC., 2006. Accountability protocols: Formalized and verified ACM Trans. Inf. Syst. Secur., v. 9
    Doi: 10.1145/1151414.1151416
    •
  • Paulson, LC., 2006. Defining Functions on Equivalence Classes TOCL, v. 7
    Doi: 10.1145/1166109.1166111
    •
  • Meng, J., Quigley, C. and Paulson, LC., 2006. Automation for Interactive Proof: First Prototype Information and Computation, v. 204
    •
  • Meng, J., Quigley, C. and Paulson, LC., 2006. Automation for interactive proof: First prototype (vol 204, pg 1575, 2006) INFORM COMPUT, v. 204
    Doi: 10.1016/j.ic.2006.09.004
    •
  • Meng, J., Quigley, C. and Paulson, LC., 2006. Erratum to "Automation for interactive proof: First prototype" [Inform. and Comput. 204 (2006) 1575-1596] (DOI:10.1016/j.ic.2005.05.010) Information and Computation, v. 204
    •
  • Paulson, LC., 2006. Defining functions on equivalence classes ACM Transactions on Computational Logic, v. 7
    Doi: 10.1145/1166109.1166111
    •
  • Bella, G., Massacci, F. and Paulson, LC., 2006. Verifying the SET purchase protocols J AUTOM REASONING, v. 36
    Doi: 10.1007/s10817-005-9018-6
    •
  • Meng, J., Quigley, C. and Paulson, LC., 2006. Automation for interactive proof: First prototype INFORM COMPUT, v. 204
    Doi: 10.1016/j.ic.2005.05.010
    •

    2005

  • Bella, G., Massacci, F. and Paulson, LC., 2005. An Overview of the Verification of SET International Journal of Information Security, v. 4
    Doi: 10.1007/s10207-004-0047-7
    •
  • Ehmety, SO. and Paulson, LC., 2005. Mechanizing compositional reasoning for concurrent systems: some lessons FORM ASP COMPUT, v. 17
    Doi: 10.1007/s00165-004-0053-6
    •
  • Paulson, LC., 2005. Welcome defects as a sign of innovation? [1] Communications of the ACM, v. 48
    Doi: 10.1145/1096000.1096016
    •

    2004

  • Paulson, LC., 2004. Organizing Numerical Theories Using Axiomatic Type Classes Journal of Automated Reasoning, v. 33
    •

    2003

  • Bella, G., Massacci, F. and Paulson, LC., 2003. Verifying the SET registration protocols IEEE J SEL AREA COMM, v. 21
    Doi: 10.1109/JSAC.2002.806133
    •
  • Paulson, LC., 2003. The Relative Consistency of the Axiom of Choice — Mechanized Using Isabelle/ZF LMS Journal of Computation and Mathematics, v. 6
    •

    2002

  • Nipkow, T., Paulson, LC. and Wenzel, M., 2002. The basics LECT NOTES COMPUT SC, v. 2283
    •

    2001

  • Paulson, LC., 2001. Keep E-journals affordable COMMUNICATIONS OF THE ACM, v. 44
    •
  • Paulson, LC., 2001. Mechanizing a theory of program composition for UNITY ACM T PROGR LANG SYS, v. 23
    •
  • Paulson, LC., 2001. Relations Between Secrets: Two Formal Analyses of the Yahalom Protocol. J. Comput. Secur., v. 9
    •
  • Paulson, LC., 2001. Mechanizing a Theory of Program Composition for UNITY ACM Transactions on Programming Languages and Systems, v. 25
    •
  • Paulson, LC., 2001. A Simple Formalization and Proof for the Mutilated Chess Board Logic Journal of the IGPL, v. 9
    Doi: 10.1093/jigpal/9.3.475
    •

    2000

  • Paulson, LC., 2000. Mechanizing UNITY in Isabelle. ACM Trans. Comput. Log., v. 1
    Doi: 10.1145/343369.343370
    •
  • Roe, M., Lee, S., Christianson, B., Anderson, R., Wheeler, D., Blaze, M., Gollman, D., Gligor, V., Mao, WB., Paulson, L. and Kuhn, M., 2000. Performance of protocols (Transcript of discussion) SECURITY PROTOCOLS, v. 1796
    •
  • Fleuriot, JD. and Paulson, LC., 2000. Mechanizing Nonstandard Real Analysis LMS Journal of Computation and Mathematics, v. 3
    •
  • Bergadano, F., Morris, B., Roe, M., Lomas, M., Blaze, M., Lee, S., Christianson, B. and Paulson, L., 2000. Issues in multicast security SECURITY PROTOCOLS, v. 1796
    •

    1999

  • Paulson, LC., 1999. Inductive Analysis of the Internet Protocol TLS. ACM Trans. Inf. Syst. Secur., v. 2
    Doi: 10.1145/322510.322530
    •
  • Kammuller, F. and Paulson, LC., 1999. A formal proof of Sylow's theorem - An experiment in abstract algebra with Isabelle HOL J AUTOM REASONING, v. 23
    •
  • Paulson, LC., 1999. A Generic Tableau Prover and its Integration with Isabelle Journal of Universal Computer Science, v. 5
    •
  • Ballarin, C. and Paulson, LC., 1999. A Pragmatic Approach to Extending Provers by Computer Algebra - with Applications to Coding Theory. Fundam. Informaticae, v. 39
    Doi: 10.3233/FI-1999-391201
    •
  • Kammüller, F. and Paulson, LC., 1999. A Formal Proof of Sylow’s theorem: An Experiment in Abstract Algebra with Isabelle HOL Journal of Automated Reasoning, v. 23
    Doi: 10.1023/A:1006269330992
    •
  • Lamport, L. and Paulson, LC., 1999. Should Your Specification Language Be Typed? ACM Transactions on Programming Languages and Systems, v. 21
    •
  • Paulson, LC., 1999. Final coalgebras as greatest fixed points in ZF set theory. Math. Struct. Comput. Sci., v. 9
    •

    1998

  • Paulson, LC., 1998. The Inductive Approach to Verifying Cryptographic Protocols. J. Comput. Secur., v. 6
    •

    1997

  • Paulson, LC., 1997. Mechanizing coinduction and corecursion in higher-order logic J LOGIC COMPUT, v. 7
    •
  • Paulson, L., 1997. Cobol in question COMMUNICATIONS OF THE ACM, v. 40
    •

    1996

  • Paulson, LC. and Grabczewski, K., 1996. Mechanizing Set Theory. J. Autom. Reason., v. 17
    •
  • Paulson, LC. and cabczewski, KG., 1996. Mechanizing Set Theory: Cardinal Arithmetic and the Axiom of Choice Journal of Automated Reasoning, v. 17
    •

    1995

  • Paulson, LC., 1995. A Concrete Final Coalgebra Theorem for ZF Set Theory. CoRR, v. abs/cs/9511103
    •
  • Paulson, LC., 1995. Set Theory for Verification: II. Induction and Recursion Journal of Automated Reasoning, v. 15
    •
  • PAULSON, LC., 1995. SET-THEORY FOR VERIFICATION .2. INDUCTION AND RECURSION J AUTOM REASONING, v. 15
    •

    1993

  • Paulson, LC., 1993. Set Theory for Verification: I. From Foundations to Functions Journal of Automated Reasoning, v. 11
    •
  • PAULSON, LC., 1993. SET-THEORY FOR VERIFICATION .1. FROM FOUNDATIONS TO FUNCTIONS J AUTOM REASONING, v. 11
    •

    1992

  • NIPKOW, T. and PAULSON, LC., 1992. ISABELLE-91 LECT NOTES ARTIF INT, v. 607
    •

    1990

  • PAULSON, LC., 1990. A FORMULATION OF THE SIMPLE THEORY OF TYPES (FOR ISABELLE) LECT NOTES COMPUT SC, v. 417
    •

    1989

  • PAULSON, L., COHEN, A. and GORDON, M., 1989. PROGRAM VERIFICATION - THE VERY IDEA COMMUNICATIONS OF THE ACM, v. 32
    •
  • Paulson, LC., 1989. The Foundation of a Generic Theorem Prover. J. Autom. Reason., v. 5
    Doi: 10.1007/BF00248324
    •
  • Paulson, LC., 1989. The Foundation of a Generic Theorem Prover Journal of Automated Reasoning, v. 5
    •

    1988

  • PAULSON, LC., 1988. ISABELLE - THE NEXT 700 THEOREM PROVERS LECT NOTES COMPUT SC, v. 310
    •

    1987

  • Paulson, LC., 1987. Logic and Computation
    Doi: 10.1017/cbo9780511526602
    •

    1986

  • Paulson, LC., 1986. Proving Termination of Normalization Functions for Conditional Experessions. J. Autom. Reason., v. 2
    Doi: 10.1007/BF00246023
    •
  • Paulson, LC., 1986. Proving Termination of Normalization Functions for Conditional Expressions Journal of Automated Reasoning, v. 2
    Doi: 10.1007/BF00246023
    •
  • Paulson, LC., 1986. Natural Deduction as Higher-order Resolution Journal of Logic Programming, v. 3
    •
  • Paulson, LC., 1986. Constructing Recursion Operators in Intuitionistic Type Theory. J. Symb. Comput., v. 2
    Doi: 10.1016/S0747-7171(86)80002-5
    •
  • PAULSON, LC., 1986. CONSTRUCTING RECURSION OPERATORS IN INTUITIONISTIC TYPE THEORY J SYMB COMPUT, v. 2
    •

    1985

  • Paulson, LC., 1985. Verifying the Unification Algorithm in LCF Science of Computer Programming, v. 5
    •
  • Paulson, LC., 1985. Lessons learned from LCF: a Survey of Natural Deduction Proofs Computer Journal, v. 28
    •

    1983

  • Paulson, LC., 1983. A Higher-Order Implementation of Rewriting Science of Computer Programming, v. 3
    •

    1896

  • Macfarlane, A., 1896. QUATERNIONS. Science, v. 3
    Doi: 10.1126/science.3.55.99
    •
    Internet publications

    2018 (No publication date)

  • Paulson, LC., 2018 (No publication date). Home Page
    • Software

    2017

  • Gordon, MJC. and Paulson, LC., 2017. HOL88 proof assistant
    Doi: 10.17863/CAM.10246
    •

    2016

  • Paulson, LC., 2016. Isabelle-89 - source code from the interactive theorem prover Isabelle upon its release in 1989
    Doi: 10.17863/CAM.9037
    •
  • Paulson, LC., 2016. Isabelle-86 - source code from the interactive theorem prover Isabelle upon its original release in 1986
    Doi: 10.17863/CAM.9039
    •
    Datasets

    2016 (No publication date)

  • Paulson, LC., 2016 (No publication date). Research data supporting "A semantics-directed compiler generator"
    • Books

    2010

  • Kaufmann, M. and Paulson, L., 2010. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics): Preface
  • 2010. Interactive Theorem Proving
    Doi: 10.1007/978-3-642-14052-5
    •

    1996

  • Paulson, LC., 1996. ML for the Working Programmer

    • 1994

  • Paulson, LC., 1994. Isabelle: A Generic Theorem Prover

    • 1991

  • Paulson, LC., 1991. ML for the Working Programmer

    • 1987

  • Paulson, LC., 1987. Logic and Computation: Interactive proof with Cambridge LCF
    • Reports

    1997

  • Paulson, LC., 1997. Mechanized Proofs of Security Protocols: Needham-Schroeder with Public Keys

    • 1996

  • Paulson, LC., 1996. A Simple Formalization and Proof for the Mutilated Chess Board

    • 1993

  • Paulson, LC., 1993. Introduction to Isabelle
  • Paulson, LC., 1993. The Isabelle Reference Manual
  • Paulson, LC., 1993. Isabelle’s Object-Logics
  • Paulson, LC., 1993. A Fixedpoint Approach to Implementing (Co)Inductive Definitions

    • 1992

  • Paulson, LC., 1992. Set Theory as a Computational Logic: I. From Foundations to Functions

    • 1990

  • Paulson, LC. and Nipkow, T., 1990. Isabelle Tutorial and User’s Manual

    • 1988

  • Paulson, LC., 1988. A preliminary user’s manual for Isabelle
    • Theses / dissertations

    1981

  • Paulson, LC., 1981. A Compiler Generator for Semantic Grammars
    • Read more at: Dr Carlos Molina-Jimenez

    Dr Carlos Molina-Jimenez

    Department of Computer Science and Technology
    University of Cambridge
    William Gates Building
    15 JJ Thomson Avenue
    Cambridge
    CB3 0FD

    About the department

    Study here
    Research
    News
    Jobs
    How to get here
    About the department

    Contact us

    Website privacy policy

    Social media

    Athena Swan bronze award logo

    Study at Cambridge

    About the University

    Research at Cambridge