Search

Your search keyword '"Aspinall, D."' showing total 272 results
Start Over Author "Aspinall, D."
272 results on '"Aspinall, D."'

15. Narrating Formal Proof (Work in Progress)

Author

Tankink, C., Geuvers, J.H., McKinna, J., Aspinall, D., Sacerdoti Coen, C., Aspinall, D., and Formal System Analysis

Subjects
General Computer Science, Computer science, business.industry, Data Science, Work in process, Data structure, Formal proof, Theoretical Computer Science, World Wide Web, Software, Work (electrical), Coursebooks, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, ComputingMethodologies_DOCUMENTANDTEXTPROCESSING, Artificial intelligence, Proof Assistants, Proof Communication, business, Computer Science(all)
Abstract

Building on existing work in proxying interaction with proof assistants, we have previously developed a proof movie. We have now considered the problem of how to augment this movie data structure to support commentary on formal proof development. In this setting, we have studied extracting commentary from an online text by Pierce et al. [Pierce, B. C., C. Casinghino and M. Greenberg, Software foundations, Course notes, online at http://www.cis.upenn.edu/~bcpierce/sf/ (2010).]. Keywords: Coursebooks; Proof Assistants; Proof Communication

Published
2012

26. Properties of instruction set processor

Author

Aspinall, D., Goos, G., editor, Hartmanis, J., editor, Brauer, W., editor, Brinch Hansen, P., editor, Gries, D., editor, Moler, C., editor, Seegmüller, G., editor, Stoer, J., editor, Wirth, N., editor, Flynn, Michael J., editor, Harris, Neville R., editor, and McCarthy, Daniel P., editor

Published
1982
Full Text
View/download PDF

30. Automated Reasoning Service for HOL Light

Author

Kaliszyk, C., Urban, J., Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W., Carette, J., Aspinall, D., Lange, C., Sojka, P., and Windsteiger, W.

Subjects
Structure (mathematical logic), Service (systems architecture), Theoretical computer science, Computer science, Programming language, Interface (Java), Data Science, HOL, computer.software_genre, Mathematical proof, Task (computing), Asynchronous communication, Lecture Notes in Computer Science, Automated reasoning, computer
Abstract

HOL(y)Hammer is an AI/ATP service for formal (computer-understandable) mathematics encoded in the HOL Light system, in particular for the users of the large Flyspeck library. The service uses several automated reasoning systems combined with several premise selection methods trained on previous Flyspeck proofs, to attack a new conjecture that uses the concepts defined in the Flyspeck library. The public online incarnation of the service runs on a 48-CPU server, currently employing in parallel for each task 25 AI/ATP combinations and 4 decision procedures that contribute to its overall performance. The system is also available for local installation by interested users, who can customize it for their own proof development. An Emacs interface allowing parallel asynchronous queries to the service is also provided. The overall structure of the service is outlined, problems that arise are discussed, and an initial account of using the system is given.

Published
2013

34. Formal mathematics on display : a wiki for Flyspeck

Author

Tankink, C., Kaliszyk, C., Urban, J., Geuvers, J.H., Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W., Formal System Analysis, and Carette, J.

Subjects
Computer science, Data Science, Formal mathematics, Proof assistant, Hyperlink, computer.software_genre, Formal proof, World Wide Web, Code refactoring, ComputingMethodologies_DOCUMENTANDTEXTPROCESSING, Lecture Notes in Computer Science, Agora, computer, computer.programming_language
Abstract

The Agora system is a prototype "Wiki for Formal Mathematics", with an aim to support developing and documenting large formalizations of mathematics in a proof assistant. The functions implemented in Agora include in-browser editing, strong AI/ATP proof advice, verification, and HTML rendering. The HTML rendering contains hyperlinks and provides on-demand explanation of the proof state for each proof step. In the present paper we show the prototype Flyspeck Wiki as an instance of Agora for HOL Light formalizations. The wiki can be used for formalizations of mathematics and for writing informal wiki pages about mathematics. Such informal pages may contain islands of formal text, which is used here for providing an initial cross-linking between Hales's informal Flyspeck book, and the formal Flyspeck development. The Agora platform intends to address distributed wiki-style collaboration on large formalization projects, in particular both the aspect of immediate editing, verification and rendering of formal code, and the aspect of gradual and mutual refactoring and correspondence of the initial informal text and its formalization. Here, we highlight these features within the Flyspeck Wiki.

Published
2013

35. Routine Donor Specific Antibody Monitoring in Heart Transplant Recipients - Is There a Role?

Author

Buckley, D., Aspinall, D., Carroll, R., Hayward, C., Kotlyar, E., Jabbour, A., Bart, N., Keogh, A., MacDonald, P., Muthiah, K., and Tong, W.

Subjects
*HEART transplant recipients, *GRAFT rejection, *IMMUNOGLOBULINS
Abstract

Allospecific anti-HLA antibodies are associated with rejection in heart transplant recipients. There is significant variation in monitoring of post-transplant donor specific antibody (DSA)s within transplant centres globally, with limited evidence to support surveillance practices. We reviewed our current practice of routine DSA surveillance in the early transplant period. Between Jan 2021 and Jan 2022, HLA antibody data from 355 post-transplant sera samples (One Lambda LABScreenTM Single Antigen kits, Thermo Fisher Scientific, Waltham MA USA) obtained weekly till month 1, fortnightly till month 3 (total 9 tests) or with suspected AMR thereafter were analysed. Background-adjusted mean fluorescent intensity (MFI) values at cut-off of 1000 MFI were used to determine antibody positivity. The presence of pre-transplant DSA and de novo DSA was documented. Endomyocardial biopsy results diagnosed acute cellular rejection (ACR) and antibody-mediated rejection (AMR) according to ISHLT criteria. 52 patients (male n= 37 [71.1%]; mean age 49.6 years) median follow up 291 days [IQR 73-546] were studied. Median detection of first positive de novo DSA occurred at day 40 post-transplant, earliest positive result occurred at day 3. Biopsy confirmed ACR rejection in relation to DSA status is shown in Table 1. Higher rates of moderate Grade 2R rejection was seen in patients with pre-transplant DSA (69%) in comparison to de novo DSA (40%) and no pre-transplant/no de novo DSA (37.5%) groups. Only one (1.9%) episode of AMR occurred in a patient with pre-transplant DSA. Our data questions the utility of early routine and frequent DSA screening to predict AMR events; AMR was a rare event in our single center experience. Longer term follow-up is required to assess the predictive utility for late AMR. [ABSTRACT FROM AUTHOR]

Published
2023
Full Text
View/download PDF

39. Mobile Resource Guarantees for Smart Devices

Author

Aspinall, D, Gilmore, S, Hofmann, M, Sannella, D, Stark, I, Barthe, Gilles, Burdy, Lilian, Huisman, Marieke, Lanet, Jean-Louis, and Muntean, Traian

Subjects
verification
Abstract

We present the Mobile Resource Guarantees framework: a system for ensuring that downloaded programs are free from run-time violations of resource bounds. Certificates are attached to code in the form of efficiently checkable proofs of resource bounds; in contrast to cryptographic certificates of code origin, these are independent of trust networks. A novel programming language with resource constraints encoded in function types is used to streamline the generation of proofs of resource usage.

Published
2005

Catalog

Books, media, physical & digital resources
See catalog results