Butler, D.; Lochbihler, A.; Aspinall, D.; Gascón, A. Formalising \(\varSigma\)-protocols and commitment schemes using CryptHOL. (English) Zbl 1524.94063 J. Autom. Reasoning 65, No. 4, 521-567 (2021). MSC: 94A60 68V20 PDFBibTeX XMLCite \textit{D. Butler} et al., J. Autom. Reasoning 65, No. 4, 521--567 (2021; Zbl 1524.94063) Full Text: DOI
Butler, David; Aspinall, David; Gascón, Adrià On the formalisation of \(\varSigma \)-protocols and commitment schemes. (English) Zbl 1524.94062 Nielson, Flemming (ed.) et al., Principles of security and trust. 8th international conference, POST 2019, held as part of the European joint conferences on theory and practice of software, ETAPS 2019, Prague, Czech Republic, April 6–11, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11426, 175-196 (2019). MSC: 94A60 68V20 PDFBibTeX XMLCite \textit{D. Butler} et al., Lect. Notes Comput. Sci. 11426, 175--196 (2019; Zbl 1524.94062) Full Text: DOI
Hofmann, Martin (ed.); Aspinall, David (ed.); Campbell, Brian (ed.); Stark, Ian (ed.); Stevens, Perdita (ed.) Foreword. (English) Zbl 1398.00101 Theor. Comput. Sci. 741, 1-2 (2018). MSC: 00B25 00B30 68-06 PDFBibTeX XMLCite \textit{M. Hofmann} (ed.) et al., Theor. Comput. Sci. 741, 1--2 (2018; Zbl 1398.00101) Full Text: DOI
Butler, David; Aspinall, David; Gascón, Adrià How to simulate it in Isabelle: towards formal proof for secure multi-party computation. (English) Zbl 1483.68486 Ayala-Rincón, Mauricio (ed.) et al., Interactive theorem proving. 8th international conference, ITP 2017, Brasília, Brazil, September 26–29, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10499, 114-130 (2017). MSC: 68V20 68Q10 68V15 94A60 PDFBibTeX XMLCite \textit{D. Butler} et al., Lect. Notes Comput. Sci. 10499, 114--130 (2017; Zbl 1483.68486) Full Text: DOI arXiv
Aspinall, David; Kaliszyk, Cezary What’s in a theorem name? (English) Zbl 1478.68434 Blanchette, Jasmin Christian (ed.) et al., Interactive theorem proving. 7th international conference, ITP 2016, Nancy, France, August 22–25, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9807, 459-465 (2016). MSC: 68V15 68T05 PDFBibTeX XMLCite \textit{D. Aspinall} and \textit{C. Kaliszyk}, Lect. Notes Comput. Sci. 9807, 459--465 (2016; Zbl 1478.68434) Full Text: DOI Link
Seghir, Mohamed Nassim; Aspinall, David EviCheck: digital evidence for Android. (English) Zbl 1471.68153 Finkbeiner, Bernd (ed.) et al., Automated technology for verification and analysis. 13th international symposium, ATVA 2015, Shanghai, China, October 12–15, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9364, 221-227 (2015). MSC: 68Q60 68N25 PDFBibTeX XMLCite \textit{M. N. Seghir} and \textit{D. Aspinall}, Lect. Notes Comput. Sci. 9364, 221--227 (2015; Zbl 1471.68153) Full Text: DOI Link
Obua, Steven; Fleuriot, Jacques; Scott, Phil; Aspinall, David Type inference for ZFH. (English) Zbl 1417.68191 Kerber, Manfred (ed.) et al., Intelligent computer mathematics. International conference, CICM 2015, Washington, DC, USA, July 13–17, 2015, Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9150, 87-101 (2015). MSC: 68T15 03B35 03E30 PDFBibTeX XMLCite \textit{S. Obua} et al., Lect. Notes Comput. Sci. 9150, 87--101 (2015; Zbl 1417.68191) Full Text: DOI Link
Dietrich, Dominik; Whiteside, Iain; Aspinall, David Polar: a framework for proof refactoring. (English) Zbl 1407.68434 McMillan, Ken (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 19th international conference, LPAR-19, Stellenbosch, South Africa, December 14–19, 2013. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 8312, 776-791 (2013). MSC: 68T15 68Q42 PDFBibTeX XMLCite \textit{D. Dietrich} et al., Lect. Notes Comput. Sci. 8312, 776--791 (2013; Zbl 1407.68434) Full Text: DOI
Aspinall, David; Denney, Ewen; Lüth, Christoph A semantic basis for proof queries and transformations. (English) Zbl 1406.68102 McMillan, Ken (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 19th international conference, LPAR-19, Stellenbosch, South Africa, December 14–19, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-45220-8/pbk). Lecture Notes in Computer Science 8312, 53-70 (2013). MSC: 68T15 PDFBibTeX XMLCite \textit{D. Aspinall} et al., Lect. Notes Comput. Sci. 8312, 53--70 (2013; Zbl 1406.68102) Full Text: DOI Link
Obua, Steven; Adams, Mark; Aspinall, David Capturing hiproofs in HOL light. (English) Zbl 1390.68583 Carette, Jacques (ed.) et al., Intelligent computer mathematics. MKM, Calculemus, DML, and systems and projects 2013, held as part of CICM 2013, Bath, UK, July 8–12, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-39319-8/pbk). Lecture Notes in Computer Science 7961. Lecture Notes in Artificial Intelligence, 184-199 (2013). MSC: 68T15 PDFBibTeX XMLCite \textit{S. Obua} et al., Lect. Notes Comput. Sci. 7961, 184--199 (2013; Zbl 1390.68583) Full Text: DOI arXiv
Carette, Jacques (ed.); Aspinall, David (ed.); Lange, Christoph (ed.); Sojka, Petr (ed.); Windsteiger, Wolfgang (ed.) Intelligent computer mathematics. MKM, Calculemus, DML, and systems and projects 2013, held as part of CICM 2013, Bath, UK, July 8–12, 2013. Proceedings. (English) Zbl 1268.68008 Lecture Notes in Computer Science 7961. Lecture Notes in Artificial Intelligence. Berlin: Springer (ISBN 978-3-642-39319-8/pbk). xv, 384 p. (2013). MSC: 68-06 68Txx 00B25 PDFBibTeX XMLCite \textit{J. Carette} (ed.) et al., Intelligent computer mathematics. MKM, Calculemus, DML, and systems and projects 2013, held as part of CICM 2013, Bath, UK, July 8--12, 2013. Proceedings. Berlin: Springer (2013; Zbl 1268.68008) Full Text: DOI
Aspinall, David (ed.); Sacerdoti Coen, Claudio (ed.) Proceedings of the 9th international workshop on user interfaces for theorem provers (UITP10), Edinburgh, UK, July 15, 2010. (English) Zbl 1284.68005 Electronic Notes in Theoretical Computer Science 285. Amsterdam: Elsevier. 120 p., electronic only (2012). MSC: 68-06 68T15 68U35 00B25 PDFBibTeX XMLCite \textit{D. Aspinall} (ed.) and \textit{C. Sacerdoti Coen} (ed.), Proceedings of the 9th international workshop on user interfaces for theorem provers (UITP10), Edinburgh, UK, July 15, 2010. Amsterdam: Elsevier (2012; Zbl 1284.68005) Full Text: Link
Whiteside, Iain; Aspinall, David; Grov, Gudmund An essence of SSReflect. (English) Zbl 1360.68770 Jeuring, Johan (ed.) et al., Intelligent computer mathematics. 11th international conference, AISC 2012, 19th symposium, Calculemus 2012, 5th international workshop, DML 2012, 11th international conference, MKM 2012, systems and projects, held as part of CICM 2012, Bremen, Germany, July 8–13, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-31373-8/pbk). Lecture Notes in Computer Science 7362. Lecture Notes in Artificial Intelligence, 186-201 (2012). MSC: 68T15 PDFBibTeX XMLCite \textit{I. Whiteside} et al., Lect. Notes Comput. Sci. 7362, 186--201 (2012; Zbl 1360.68770) Full Text: DOI
Aspinall, David; Denney, Ewen; Lüth, Christoph Querying proofs. (English) Zbl 1352.68212 Bjørner, Nikolaj (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 18th international conference, LPAR-18, Mérida, Venezuela, March 11–15, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-28716-9/pbk). Lecture Notes in Computer Science 7180, 92-106 (2012). MSC: 68T15 PDFBibTeX XMLCite \textit{D. Aspinall} et al., Lect. Notes Comput. Sci. 7180, 92--106 (2012; Zbl 1352.68212) Full Text: DOI
Whiteside, Iain; Aspinall, David; Dixon, Lucas; Grov, Gudmund Towards formal proof script refactoring. (English) Zbl 1335.68240 Davenport, James H. (ed.) et al., Intelligent computer mathematics. 18th symposium, Calculemus 2011, and 10th international conference, MKM 2011, Bertinoro, Italy, July 18–23, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-22672-4/pbk). Lecture Notes in Computer Science 6824. Lecture Notes in Artificial Intelligence, 260-275 (2011). MSC: 68T15 PDFBibTeX XMLCite \textit{I. Whiteside} et al., Lect. Notes Comput. Sci. 6824, 260--275 (2011; Zbl 1335.68240) Full Text: DOI Link
Aspinall, David; Denney, Ewen; Lüth, Christoph Tactics for hierarchical proof. (English) Zbl 1205.68359 Math. Comput. Sci. 3, No. 3, 309-330 (2010). MSC: 68T15 PDFBibTeX XMLCite \textit{D. Aspinall} et al., Math. Comput. Sci. 3, No. 3, 309--330 (2010; Zbl 1205.68359) Full Text: DOI
Keighren, Gavin; Aspinall, David; Steel, Graham Towards a type system for security APIs. (English) Zbl 1252.68110 Degano, Pierpaolo (ed.) et al., Foundations and applications of security analysis. Joint workshop on automated reasoning for security protocol analysis and issues in the theory of security, ARSPA-WITS 2009, York, UK, March 28–29, 2009. Revised selected papers. Berlin: Springer (ISBN 978-3-642-03458-9/pbk). Lecture Notes in Computer Science 5511, 173-192 (2009). MSC: 68P25 68N30 PDFBibTeX XMLCite \textit{G. Keighren} et al., Lect. Notes Comput. Sci. 5511, 173--192 (2009; Zbl 1252.68110) Full Text: DOI
Aspinall, David; Maier, Patrick; Stark, Ian Safety guarantees from explicit resource management. (English) Zbl 1209.68119 de Boer, Frank S. (ed.) et al., Formal methods for components and objects. 6th international symposium, FMCO 2007, Amsterdam, The Netherlands, October 24–26, 2007. Revised lectures. Berlin: Springer (ISBN 978-3-540-92187-5/pbk). Lecture Notes in Computer Science 5382, 52-71 (2008). MSC: 68N30 PDFBibTeX XMLCite \textit{D. Aspinall} et al., Lect. Notes Comput. Sci. 5382, 52--71 (2008; Zbl 1209.68119) Full Text: DOI
Aspinall, David; Denney, Ewen; Lüth, Christoph A tactic language for hiproofs. (English) Zbl 1166.68336 Autexier, Serge (ed.) et al., Intelligent computer mathematics. 9th international conference, AISC 2008, 15th symposium, Calculemus 2008, 7th international conference, MKM 2008, Birmingham, UK, July 28–August 1, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-85109-7/pbk). Lecture Notes in Computer Science 5144. Lecture Notes in Artificial Intelligence, 339-354 (2008). MSC: 68T15 PDFBibTeX XMLCite \textit{D. Aspinall} et al., Lect. Notes Comput. Sci. 5144, 339--354 (2008; Zbl 1166.68336) Full Text: DOI
Aspinall, David; Hofmann, Martin; Konečný, Michal A type system with usage aspects. (English) Zbl 1142.68019 J. Funct. Program. 18, No. 2, 141-178 (2008). MSC: 68N18 PDFBibTeX XMLCite \textit{D. Aspinall} et al., J. Funct. Program. 18, No. 2, 141--178 (2008; Zbl 1142.68019) Full Text: DOI
Aspinall, David; Hoffman, Piotr Datatypes in memory. (English) Zbl 1214.68228 Mossakowski, Till (ed.) et al., Algebra and coalgebra in computer science. Second international conference, CALCO 2007, Bergen, Norway, August 20–24, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-73857-2/pbk). Lecture Notes in Computer Science 4624, 111-125 (2007). MSC: 68Q65 68Q60 PDFBibTeX XMLCite \textit{D. Aspinall} and \textit{P. Hoffman}, Lect. Notes Comput. Sci. 4624, 111--125 (2007; Zbl 1214.68228) Full Text: DOI
Aspinall, David; Ševčík, Jaroslav Formalising Java’s data race free guarantee. (English) Zbl 1144.68304 Schneider, Klaus (ed.) et al., Theorem proving in higher order logics. 20th international conference, TPHOLs 2007, Kaiserslautern, Germany, September 10–13, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-74590-7/pbk). Lecture Notes in Computer Science 4732, 22-37 (2007). MSC: 68N15 68N19 68T15 PDFBibTeX XMLCite \textit{D. Aspinall} and \textit{J. Ševčík}, Lect. Notes Comput. Sci. 4732, 22--37 (2007; Zbl 1144.68304) Full Text: DOI
Aspinall, David; Beringer, Lennart; Hofmann, Martin; Loidl, Hans-Wolfgang; Momigliano, Alberto A program logic for resources. (English) Zbl 1133.68010 Theor. Comput. Sci. 389, No. 3, 411-445 (2007). MSC: 68N15 03B70 PDFBibTeX XMLCite \textit{D. Aspinall} et al., Theor. Comput. Sci. 389, No. 3, 411--445 (2007; Zbl 1133.68010) Full Text: DOI Link
Aspinall, David; Lüth, Christoph; Winterstein, Daniel A framework for interactive proof. (English) Zbl 1202.68371 Kauers, Manuel (ed.) et al., Towards mechanized mathematical assistants. 14th symposium, Calculemus 2007, 6th international conference, MKM 2007, Hagenberg, Austria, June 27–30, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-73083-5/pbk). Lecture Notes in Computer Science 4573. Lecture Notes in Artificial Intelligence, 161-175 (2007). MSC: 68T15 PDFBibTeX XMLCite \textit{D. Aspinall} et al., Lect. Notes Comput. Sci. 4573, 161--175 (2007; Zbl 1202.68371) Full Text: DOI
Aspinall, David; Lüth, Christoph; Wolff, Burkhart Assisted proof document authoring. (English) Zbl 1151.68658 Kohlhase, Michael (ed.), Mathematical knowledge management. 4th international conference, MKM 2005, Bremen, Germany, July 15-17, 2005. Revised selected papers. Berlin: Springer (ISBN 3-540-31430-X/pbk). Lecture Notes in Computer Science 3863. Lecture Notes in Artificial Intelligence, 65-80 (2006). MSC: 68T30 68T15 PDFBibTeX XMLCite \textit{D. Aspinall} et al., Lect. Notes Comput. Sci. 3863, 65--80 (2006; Zbl 1151.68658) Full Text: DOI
Aspinall, David; Beringer, Lennart; Hofmann, Martin; Loidl, Hans-Wolfgang; Momigliano, Alberto A program logic for resource verification. (English) Zbl 1099.68584 Slind, Konrad (ed.) et al., Theorem proving in higher order logics. 17th international conference, TPHOLs 2004, Park City, Utah, USA, September 14–17, 2004. Proceedings. Berlin: Springer (ISBN 3-540-23017-3/pbk). Lecture Notes in Computer Science 3223, 34-49 (2004). MSC: 68N30 03B70 68N18 68T15 PDFBibTeX XMLCite \textit{D. Aspinall} et al., Lect. Notes Comput. Sci. 3223, 34--49 (2004; Zbl 1099.68584) Full Text: DOI
Aspinall, David Type checking parametrised programs and specifications in \(\text{ASL}+_{\text{FPC}}\). (English) Zbl 1278.68201 Wirsing, Martin (ed.) et al., Recent trends in algebraic development techniques. 16th international workshop, WADT 2002, Frauenchiemsee, Germany, September 24–27, 2002. Revised selected papers. Berlin: Springer (ISBN 3-540-20537-3/pbk). Lect. Notes Comput. Sci. 2755, 129-144 (2003). MSC: 68Q65 68N30 PDFBibTeX XMLCite \textit{D. Aspinall}, Lect. Notes Comput. Sci. 2755, 129--144 (2003; Zbl 1278.68201) Full Text: DOI
Aspinall, David; Compagnoni, Adriana Heap-bounded assembly language. (English) Zbl 1069.68033 J. Autom. Reasoning 31, No. 3-4, 261-302 (2003). MSC: 68N15 68N30 68T15 PDFBibTeX XMLCite \textit{D. Aspinall} and \textit{A. Compagnoni}, J. Autom. Reasoning 31, No. 3--4, 261--302 (2003; Zbl 1069.68033) Full Text: DOI
Aspinall, David; Hofmann, Martin Another type system for in-place update. (English) Zbl 1077.68565 Le Métayer, Daniel (ed.), Programming languages and systems. 11th European symposium on programming, ESOP 2002, held as part of the joint European conferences on theory and practice of software, ETAPS 2002, Grenoble, France, April 8–12, 2002. Proceedings. Berlin: Springer (ISBN 3-540-43363-5). Lect. Notes Comput. Sci. 2305, 36-52 (2002). MSC: 68N18 68Q55 PDFBibTeX XMLCite \textit{D. Aspinall} and \textit{M. Hofmann}, Lect. Notes Comput. Sci. 2305, 36--52 (2002; Zbl 1077.68565) Full Text: Link
Aspinall, D.; Compagnoni, A. Subtyping dependent types. (English) Zbl 0989.68020 Theor. Comput. Sci. 266, No. 1-2, 273-309 (2001). MSC: 68N18 PDFBibTeX XMLCite \textit{D. Aspinall} and \textit{A. Compagnoni}, Theor. Comput. Sci. 266, No. 1--2, 273--309 (2001; Zbl 0989.68020) Full Text: DOI
Aspinall, David Subtyping with power types. (English) Zbl 0973.03018 Clote, Peter G. (ed.) et al., Computer science logic. 14th international workshop, CSL 2000. Annual conference of the EACSL, Fischbachau, Germany, August 21-26, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1862, 156-171 (2000). MSC: 03B40 68N18 PDFBibTeX XMLCite \textit{D. Aspinall}, Lect. Notes Comput. Sci. 1862, 156--171 (2000; Zbl 0973.03018)
Aspinall, David Proof General: A generic tool for proof development. (English) Zbl 0971.68627 Graf, Susanne (ed.) et al., Tools and algorithms for the construction and analysis of systems. 6th international conference, TACAS 2000. Held as part of the joint European conferences on theory and practice of software, ETAPS 2000, Berlin, Germany, March 25 - April 2, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1785, 38-42 (2000). MSC: 68U99 68T15 PDFBibTeX XMLCite \textit{D. Aspinall}, Lect. Notes Comput. Sci. 1785, 38--42 (2000; Zbl 0971.68627)
Aspinall, David Subtyping with singleton types. (English) Zbl 1044.68541 Pacholski, Leszek (ed.) et al., Computer science logic. 8th workshop, CSL ’94, Kazimierz, Poland, September 25-30, 1994. Selected papers. Berlin: Springer-Verlag (ISBN 3-540-60017-5). Lect. Notes Comput. Sci. 933, 1-15 (1995). MSC: 68N18 03B40 PDFBibTeX XMLCite \textit{D. Aspinall}, Lect. Notes Comput. Sci. 933, 1--15 (1995; Zbl 1044.68541)
Dagless, Erik L. (ed.); Aspinall, David (ed.) Introduction to microcomputers. (English) Zbl 0521.68002 A Pitman International Text. London: Pitman. XI, 244 p. £5.95 (1982). MSC: 68-02 68N99 PDFBibTeX XML
Dagless, E. L.; Aspinall, D. Introduction to microcomputers. (English) Zbl 0512.68007 Digital System Design Series. Rockville, Maryland (USA): Computer Science Press. XI, 243 p. (1982). MSC: 68N99 PDFBibTeX XML
Aspinall, D. (ed.) The microprocessor and its application. An advanced course. (English) Zbl 0394.68002 Cambridge etc.: Cambridge University Press. XVIII, 383 p. £12.50 (1978). MSC: 68-02 68N99 PDFBibTeX XML
Aspinall, D. (ed.); Dagless, E. L. (ed.) Introduction to microprocessors. (English) Zbl 0377.68003 London: Pitman. New York: Academic Press. VII, 162 p. £5.50 (1977). MSC: 68-01 PDFBibTeX XML