×
Author ID: aspinall.david Recent zbMATH articles by "Aspinall, David"
Published as: Aspinall, David; Aspinall, D.

Publications by Year

Citations contained in zbMATH Open

19 Publications have been cited 99 times in 87 Documents Cited by Year
Proof General: A generic tool for proof development. Zbl 0971.68627
Aspinall, David
23
2000
Subtyping dependent types. Zbl 0989.68020
Aspinall, D.; Compagnoni, A.
16
2001
A program logic for resources. Zbl 1133.68010
Aspinall, David; Beringer, Lennart; Hofmann, Martin; Loidl, Hans-Wolfgang; Momigliano, Alberto
11
2007
Subtyping with singleton types. Zbl 1044.68541
Aspinall, David
8
1995
A framework for interactive proof. Zbl 1202.68371
Aspinall, David; Lüth, Christoph; Winterstein, Daniel
7
2007
Formalising Java’s data race free guarantee. Zbl 1144.68304
Aspinall, David; Ševčík, Jaroslav
6
2007
Assisted proof document authoring. Zbl 1151.68658
Aspinall, David; Lüth, Christoph; Wolff, Burkhart
3
2006
Towards formal proof script refactoring. Zbl 1335.68240
Whiteside, Iain; Aspinall, David; Dixon, Lucas; Grov, Gudmund
3
2011
Type inference for ZFH. Zbl 1417.68191
Obua, Steven; Fleuriot, Jacques; Scott, Phil; Aspinall, David
3
2015
A type system with usage aspects. Zbl 1142.68019
Aspinall, David; Hofmann, Martin; Konečný, Michal
3
2008
A program logic for resource verification. Zbl 1099.68584
Aspinall, David; Beringer, Lennart; Hofmann, Martin; Loidl, Hans-Wolfgang; Momigliano, Alberto
2
2004
Querying proofs. Zbl 1352.68212
Aspinall, David; Denney, Ewen; Lüth, Christoph
2
2012
Polar: a framework for proof refactoring. Zbl 1407.68434
Dietrich, Dominik; Whiteside, Iain; Aspinall, David
2
2013
Tactics for hierarchical proof. Zbl 1205.68359
Aspinall, David; Denney, Ewen; Lüth, Christoph
2
2010
Capturing hiproofs in HOL light. Zbl 1390.68583
Obua, Steven; Adams, Mark; Aspinall, David
2
2013
How to simulate it in Isabelle: towards formal proof for secure multi-party computation. Zbl 1483.68486
Butler, David; Aspinall, David; Gascón, Adrià
2
2017
What’s in a theorem name? Zbl 1478.68434
Aspinall, David; Kaliszyk, Cezary
2
2016
Heap-bounded assembly language. Zbl 1069.68033
Aspinall, David; Compagnoni, Adriana
1
2003
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
How to simulate it in Isabelle: towards formal proof for secure multi-party computation. Zbl 1483.68486
Butler, David; Aspinall, David; Gascón, Adrià
2
2017
What’s in a theorem name? Zbl 1478.68434
Aspinall, David; Kaliszyk, Cezary
2
2016
Type inference for ZFH. Zbl 1417.68191
Obua, Steven; Fleuriot, Jacques; Scott, Phil; Aspinall, David
3
2015
Polar: a framework for proof refactoring. Zbl 1407.68434
Dietrich, Dominik; Whiteside, Iain; Aspinall, David
2
2013
Capturing hiproofs in HOL light. Zbl 1390.68583
Obua, 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.68212
Aspinall, David; Denney, Ewen; Lüth, Christoph
2
2012
Towards formal proof script refactoring. Zbl 1335.68240
Whiteside, Iain; Aspinall, David; Dixon, Lucas; Grov, Gudmund
3
2011
Tactics for hierarchical proof. Zbl 1205.68359
Aspinall, David; Denney, Ewen; Lüth, Christoph
2
2010
A type system with usage aspects. Zbl 1142.68019
Aspinall, David; Hofmann, Martin; Konečný, Michal
3
2008
A program logic for resources. Zbl 1133.68010
Aspinall, David; Beringer, Lennart; Hofmann, Martin; Loidl, Hans-Wolfgang; Momigliano, Alberto
11
2007
A framework for interactive proof. Zbl 1202.68371
Aspinall, David; Lüth, Christoph; Winterstein, Daniel
7
2007
Formalising Java’s data race free guarantee. Zbl 1144.68304
Aspinall, David; Ševčík, Jaroslav
6
2007
Assisted proof document authoring. Zbl 1151.68658
Aspinall, David; Lüth, Christoph; Wolff, Burkhart
3
2006
A program logic for resource verification. Zbl 1099.68584
Aspinall, David; Beringer, Lennart; Hofmann, Martin; Loidl, Hans-Wolfgang; Momigliano, Alberto
2
2004
Heap-bounded assembly language. Zbl 1069.68033
Aspinall, David; Compagnoni, Adriana
1
2003
Subtyping dependent types. Zbl 0989.68020
Aspinall, D.; Compagnoni, A.
16
2001
Proof General: A generic tool for proof development. Zbl 0971.68627
Aspinall, David
23
2000
Subtyping with singleton types. Zbl 1044.68541
Aspinall, David
8
1995
all top 5

Cited by 151 Authors

7 Aspinall, David
6 Kaliszyk, Cezary
4 Rabe, Florian
4 Sacerdoti Coen, Claudio
4 Tassi, Enrico
4 Wenzel, Makarius
3 Beringer, Lennart
3 Compagnoni, Adriana B.
3 Fleuriot, Jacques D.
3 Grov, Gudmund
3 Hofmann, Martin
3 Montenegro, Manuel
3 Paulson, Lawrence Charles
3 Peña, Ricardo
3 Segura, Clara
2 Asperti, Andrea
2 Barthe, Gilles
2 Benzmüller, Christoph Ewald
2 Chen, Gang
2 Kohlhase, Michael
2 Lochbihler, Andreas
2 Loidl, Hans-Wolfgang
2 Luo, Zhaohui
2 Meikle, Laura I.
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 Atkey, Robert
1 Autexier, Serge
1 Barras, Bruno
1 Basin, David A.
1 Belo, João Filipe
1 Bonfante, Guillaume
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 Kahle, Reinhard
1 Kamareddine, Fairouz D.
1 Kawash, Jalal
1 Kersten, Rody
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 Lüth, Christoph
1 Maier, Patrick
1 Marion, Jean-Yves
1 Meng, Jia
1 Minari, Pierluigi
...and 51 more Authors

Citations by Year