×

zbMATH — the first resource for mathematics

Aspinall, David

Compute Distance To:
Author ID: aspinall.david Recent zbMATH articles by "Aspinall, David"
Published as: Aspinall, D.; Aspinall, David
Documents Indexed: 35 Publications since 1977, including 6 Books

Publications by Year

Citations contained in zbMATH

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

Cited by 122 Authors

6 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 Segura, Clara
3 Tassi, Enrico
2 Asperti, Andrea
2 Barthe, Gilles
2 Benzmüller, Christoph Ewald
2 Fleuriot, Jacques D.
2 Grov, Gudmund
2 Luo, Zhaohui
2 Nipkow, Tobias
2 Pąk, Karol
2 Rabe, Florian
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 Chen, Gang
1 Chen, Gang
1 Cheng, Steven
1 Coquand, Thierry
1 Courant, Judicaël
1 Czajka, Łukasz
1 Dabrowski, Frédéric
1 David, René
1 Dehaye, Paul-Olivier
1 Denney, Ewen
1 Dennis, Louise Abigail
1 Dietrich, Dominik
1 Dixon, Lucas
1 Dockins, Robert
1 Farmer, William M.
1 Feng, Xinyu
1 Gast, Holger
1 Gauthier, Thibault
1 Goguen, Healfdene
1 Gordon, Andrew D.
1 Greenberg, Michael D.
1 Heeren, Bastiaan
1 Heras, Jónathan
1 Higham, Lisa
1 Hobor, Aquinas
1 Hupel, Lars
1 Iancu, Mihnea
1 Igarashi, Atsushi
1 Janssens, Gerda
1 Jensen, Thomas P.
1 Jeuring, Johan
1 Jobin, Arnaud
1 Kawash, Jalal
1 Kohlhase, Michael
1 Komendantskaya, Ekaterina
1 Konečný, Michal
1 Konovalov, Alexander B.
1 Kurata, Toshihiko
1 Lelièvre, Samuel
1 Lin, Yuhui
1 Lochbihler, Andreas
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 H.
1 Müller, Dennis
1 Narboux, Julien
1 Obua, Steven
1 Pagano, Miguel
1 Parlato, Gennaro
1 Pavlova, Mariela
1 Pfeiffer, Markus
1 Phan, Quan
1 Pichardie, David
1 Pierce, Benjamin C.
1 Pottier, François
1 Pucella, Riccardo
1 Quigley, Claire
...and 22 more Authors

Citations by Year