Edit Profile (opens in new tab) Aspinall, David Compute Distance To: Compute Author ID: aspinall.david Published as: Aspinall, David; Aspinall, D. Documents Indexed: 30 Publications since 1982, including 1 Book 6 Contributions as Editor Co-Authors: 36 Co-Authors with 31 Joint Publications 480 Co-Co-Authors all top 5 Co-Authors 5 single-authored 6 Lüth, Christoph 5 Hofmann, Martin 4 Denney, Ewen 3 Dagless, Erik L. 3 Whiteside, Iain 2 Beringer, Lennart 2 Compagnoni, Adriana B. 2 Gascón, Adrià 2 Grov, Gudmund 2 Loidl, Hans-Wolfgang 2 Momigliano, Alberto 2 Obua, Steven 2 Stark, Ian 1 Adams, Mark 1 Campbell, Brian A. 1 Carette, Jacques 1 Dietrich, Dominik 1 Dixon, Lucas 1 Fleuriot, Jacques D. 1 Hoffman, Piotr 1 Kaliszyk, Cezary 1 Keighren, Gavin 1 Konečný, Michal 1 Lange, Christoph 1 Lochbihler, Andreas 1 Maier, Patrick 1 Sacerdoti Coen, Claudio 1 Scott, Phil 1 Seghir, Mohamed Nassim 1 Ševčík, Jaroslav 1 Sojka, Petr 1 Steel, Graham 1 Stevens, Perdita 1 Windsteiger, Wolfgang 1 Winterstein, Daniel 1 Wolff, Burkhart all top 5 Serials 3 Theoretical Computer Science 2 Journal of Automated Reasoning 1 Journal of Functional Programming 1 Lecture Notes in Computer Science 1 Electronic Notes in Theoretical Computer Science 1 Mathematics in Computer Science Fields 36 Computer science (68-XX) 5 Mathematical logic and foundations (03-XX) 3 General and overarching topics; collections (00-XX) 1 Information and communication theory, circuits (94-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 19 Publications have been cited 89 times in 78 Documents Cited by ▼ Year ▼ Proof General: A generic tool for proof development. Zbl 0971.68627Aspinall, David 22 2000 Subtyping dependent types. Zbl 0989.68020Aspinall, D.; Compagnoni, A. 14 2001 Subtyping with singleton types. Zbl 1044.68541Aspinall, David 8 1995 A program logic for resources. Zbl 1133.68010Aspinall, David; Beringer, Lennart; Hofmann, Martin; Loidl, Hans-Wolfgang; Momigliano, Alberto 8 2007 A framework for interactive proof. Zbl 1202.68371Aspinall, David; Lüth, Christoph; Winterstein, Daniel 5 2007 Formalising Java’s data race free guarantee. Zbl 1144.68304Aspinall, David; Ševčík, Jaroslav 5 2007 Assisted proof document authoring. Zbl 1151.68658Aspinall, David; Lüth, Christoph; Wolff, Burkhart 3 2006 A type system with usage aspects. Zbl 1142.68019Aspinall, David; Hofmann, Martin; Konečný, Michal 3 2008 Type inference for ZFH. Zbl 1417.68191Obua, Steven; Fleuriot, Jacques; Scott, Phil; Aspinall, David 3 2015 Towards formal proof script refactoring. Zbl 1335.68240Whiteside, Iain; Aspinall, David; Dixon, Lucas; Grov, Gudmund 3 2011 How to simulate it in Isabelle: towards formal proof for secure multi-party computation. Zbl 1483.68486Butler, David; Aspinall, David; Gascón, Adrià 2 2017 Tactics for hierarchical proof. Zbl 1205.68359Aspinall, David; Denney, Ewen; Lüth, Christoph 2 2010 A program logic for resource verification. Zbl 1099.68584Aspinall, David; Beringer, Lennart; Hofmann, Martin; Loidl, Hans-Wolfgang; Momigliano, Alberto 2 2004 Polar: a framework for proof refactoring. Zbl 1407.68434Dietrich, Dominik; Whiteside, Iain; Aspinall, David 2 2013 Capturing hiproofs in HOL light. Zbl 1390.68583Obua, Steven; Adams, Mark; Aspinall, David 2 2013 What’s in a theorem name? Zbl 1478.68434Aspinall, David; Kaliszyk, Cezary 2 2016 Intelligent computer mathematics. MKM, Calculemus, DML, and systems and projects 2013, held as part of CICM 2013, Bath, UK, July 8–12, 2013. Proceedings. Zbl 1268.68008 1 2013 Heap-bounded assembly language. Zbl 1069.68033Aspinall, David; Compagnoni, Adriana 1 2003 Querying proofs. Zbl 1352.68212Aspinall, David; Denney, Ewen; Lüth, Christoph 1 2012 How to simulate it in Isabelle: towards formal proof for secure multi-party computation. Zbl 1483.68486Butler, David; Aspinall, David; Gascón, Adrià 2 2017 What’s in a theorem name? Zbl 1478.68434Aspinall, David; Kaliszyk, Cezary 2 2016 Type inference for ZFH. Zbl 1417.68191Obua, Steven; Fleuriot, Jacques; Scott, Phil; Aspinall, David 3 2015 Polar: a framework for proof refactoring. Zbl 1407.68434Dietrich, Dominik; Whiteside, Iain; Aspinall, David 2 2013 Capturing hiproofs in HOL light. Zbl 1390.68583Obua, Steven; Adams, Mark; Aspinall, David 2 2013 Intelligent computer mathematics. MKM, Calculemus, DML, and systems and projects 2013, held as part of CICM 2013, Bath, UK, July 8–12, 2013. Proceedings. Zbl 1268.68008 1 2013 Querying proofs. Zbl 1352.68212Aspinall, David; Denney, Ewen; Lüth, Christoph 1 2012 Towards formal proof script refactoring. Zbl 1335.68240Whiteside, Iain; Aspinall, David; Dixon, Lucas; Grov, Gudmund 3 2011 Tactics for hierarchical proof. Zbl 1205.68359Aspinall, David; Denney, Ewen; Lüth, Christoph 2 2010 A type system with usage aspects. Zbl 1142.68019Aspinall, David; Hofmann, Martin; Konečný, Michal 3 2008 A program logic for resources. Zbl 1133.68010Aspinall, David; Beringer, Lennart; Hofmann, Martin; Loidl, Hans-Wolfgang; Momigliano, Alberto 8 2007 A framework for interactive proof. Zbl 1202.68371Aspinall, David; Lüth, Christoph; Winterstein, Daniel 5 2007 Formalising Java’s data race free guarantee. Zbl 1144.68304Aspinall, David; Ševčík, Jaroslav 5 2007 Assisted proof document authoring. Zbl 1151.68658Aspinall, David; Lüth, Christoph; Wolff, Burkhart 3 2006 A program logic for resource verification. Zbl 1099.68584Aspinall, David; Beringer, Lennart; Hofmann, Martin; Loidl, Hans-Wolfgang; Momigliano, Alberto 2 2004 Heap-bounded assembly language. Zbl 1069.68033Aspinall, David; Compagnoni, Adriana 1 2003 Subtyping dependent types. Zbl 0989.68020Aspinall, D.; Compagnoni, A. 14 2001 Proof General: A generic tool for proof development. Zbl 0971.68627Aspinall, David 22 2000 Subtyping with singleton types. Zbl 1044.68541Aspinall, David 8 1995 all cited Publications top 5 cited Publications all top 5 Cited by 136 Authors 7 Aspinall, David 6 Kaliszyk, Cezary 4 Sacerdoti Coen, Claudio 4 Wenzel, Makarius 3 Beringer, Lennart 3 Compagnoni, Adriana B. 3 Hofmann, Martin 3 Montenegro, Manuel 3 Paulson, Lawrence Charles 3 Peña, Ricardo 3 Rabe, Florian 3 Segura, Clara 3 Tassi, Enrico 2 Asperti, Andrea 2 Barthe, Gilles 2 Benzmüller, Christoph Ewald 2 Chen, Gang 2 Fleuriot, Jacques D. 2 Grov, Gudmund 2 Kohlhase, Michael 2 Lochbihler, Andreas 2 Luo, Zhaohui 2 Nipkow, Tobias 2 Pąk, Karol 2 Raffalli, Christophe 2 Zacchiroli, Stefano 1 Abel, Andreas M. 1 Adams, Robin 1 Arthan, Rob D. 1 Atig, Mohamed Faouzi 1 Autexier, Serge 1 Basin, David A. 1 Belo, João Filipe 1 Borgström, Johannes 1 Bouajjani, Ahmed 1 Brown, Chad Edward 1 Cachera, David 1 Calude, Cristian S. 1 Carette, Jacques 1 Castagna, Giuseppe 1 Charguéraud, Arthur 1 Cheng, Steven 1 Chlipala, Adam J. 1 Coquand, Thierry 1 Courant, Judicaël 1 Czajka, Łukasz 1 Dabrowski, Frédéric 1 David, Rene 1 Dehaye, Paul-Olivier 1 Delaware, Benjamin 1 Denney, Ewen 1 Dennis, Louise Abigail 1 Dietrich, Dominik 1 Dixon, Lucas 1 Dockins, Robert 1 Dong, JinSong 1 Farmer, William M. 1 Feng, Xinyu 1 Gascón, Adrià 1 Gast, Holger 1 Gauthier, Thibault 1 Gligorić, Miloš V. 1 Goguen, Healfdene 1 Gordon, Andrew D. 1 Greenberg, Michael D. 1 Gross, Jason 1 Heeren, Bastiaan 1 Heras, Jónathan 1 Higham, Lisa 1 Hoa, Koh Chuen 1 Hobor, Aquinas 1 Hou, Zhe 1 Hupel, Lars 1 Iancu, Mihnea 1 Igarashi, Atsushi 1 Janssens, Gerda 1 Jeuring, Johan 1 Jobin, Arnaud 1 Kawash, Jalal 1 Komendantskaya, Ekaterina 1 Konečný, Michal 1 Konovalov, Olexandr 1 Kurata, Toshihiko 1 Lelièvre, Samuel 1 Li, Junyi Jessy 1 Lin, Yuhui 1 Liu, Yang 1 Loidl, Hans-Wolfgang 1 Lüth, Christoph 1 Maier, Patrick 1 Meikle, Laura I. 1 Meng, Jia 1 Minari, Pierluigi 1 Momigliano, Alberto 1 Müller, Christine 1 Müller, Dennis 1 Narboux, Julien 1 Nie, Pengyu 1 Obua, Steven 1 Pagano, Miguel ...and 36 more Authors all top 5 Cited in 18 Serials 9 Journal of Automated Reasoning 7 Information and Computation 3 Journal of Functional Programming 2 Theoretical Computer Science 2 MSCS. Mathematical Structures in Computer Science 2 Journal of Applied Logic 2 Mathematics in Computer Science 1 Annals of Pure and Applied Logic 1 Journal of Symbolic Computation 1 Journal of Computer Science and Technology 1 Journal of Cryptology 1 Formal Aspects of Computing 1 Distributed Computing 1 Archive for Mathematical Logic 1 The Journal of Logic and Algebraic Programming 1 Theory and Practice of Logic Programming 1 Journal of Formalized Reasoning 1 Frontiers of Computer Science Cited in 5 Fields 76 Computer science (68-XX) 19 Mathematical logic and foundations (03-XX) 2 Mathematics education (97-XX) 1 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 1 Information and communication theory, circuits (94-XX) Citations by Year