SwePub
Sök i SwePub databas

  Utökad sökning

Träfflista för sökning "WFRF:(Adams Robin) "

Sökning: WFRF:(Adams Robin)

  • Resultat 1-10 av 32
Sortera/gruppera träfflistan
   
NumreringReferensOmslagsbildHitta
1.
  •  
2.
  • Fazey, Ioan, et al. (författare)
  • Transforming knowledge systems for life on Earth : Visions of future systems and how to get there
  • 2020
  • Ingår i: Energy Research & Social Science. - : Elsevier. - 2214-6296 .- 2214-6326. ; 70
  • Tidskriftsartikel (refereegranskat)abstract
    • Formalised knowledge systems, including universities and research institutes, are important for contemporary societies. They are, however, also arguably failing humanity when their impact is measured against the level of progress being made in stimulating the societal changes needed to address challenges like climate change. In this research we used a novel futures-oriented and participatory approach that asked what future envisioned knowledge systems might need to look like and how we might get there. Findings suggest that envisioned future systems will need to be much more collaborative, open, diverse, egalitarian, and able to work with values and systemic issues. They will also need to go beyond producing knowledge about our world to generating wisdom about how to act within it. To get to envisioned systems we will need to rapidly scale methodological innovations, connect innovators, and creatively accelerate learning about working with intractable challenges. We will also need to create new funding schemes, a global knowledge commons, and challenge deeply held assumptions. To genuinely be a creative force in supporting longevity of human and non-human life on our planet, the shift in knowledge systems will probably need to be at the scale of the enlightenment and speed of the scientific and technological revolution accompanying the second World War. This will require bold and strategic action from governments, scientists, civic society and sustained transformational intent.
  •  
3.
  • Adams, Robin, 1978 (författare)
  • A Modular Hierarchy of Logical Frameworks
  • 2004
  • Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Berlin, Heidelberg : Springer Berlin Heidelberg. - 1611-3349 .- 0302-9743. ; 3085, s. 1-16
  • Konferensbidrag (refereegranskat)abstract
    • We present a method for defining logical frameworks as a collection of features which are defined and behave independently of one another. Each feature is a set of grammar clauses and rules of deduction such that the result of adding the feature to a framework is a conservative extension of the framework itself. We show how several existing logical frameworks can be so built, and how several much weaker frameworks defined in this manner are adequate for expressing a wide variety of object logics.
  •  
4.
  • Adams, Robin, 1978, et al. (författare)
  • A pluralist approach to the formalisation of mathematics
  • 2011
  • Ingår i: Mathematical Structures in Computer Science. - 0960-1295 .- 1469-8072. ; 21:4, s. 913-942
  • Tidskriftsartikel (refereegranskat)abstract
    • We present a programme of research for pluralist formalisations, that is, formalisations that involve proving results in more than one foundation.A foundation consists of two parts: a logical part, which provides a notion of inference, and a non-logical part, which provides the entities to be reasoned about. An LTT is a formal system composed of two such separate parts. We show how LTTs may be used as the basis for a pluralist formalisation.We show how different foundations may be formalised as LTTs, and also describe a new method for proof reuse. If we know that a translation Φ exists between two logic-enriched type theories (LTTs) S and T, and we have formalised a proof of a theorem α in S, we may wish to make use of the fact that Φ(α) is a theorem of T. We show how this is sometimes possible by writing a proof script MΦ. For any proof script Mα that proves a theorem α in S, if we change Mα so it first imports MΦ, the resulting proof script will still parse, and will be a proof of Φ(α) in T.In this paper, we focus on the logical part of an LTT-framework and show how the above method of proof reuse is done for four cases of Φ: inclusion, the double negation translation, the A-translation and the Russell–Prawitz modality. This work has been carried out using the proof assistant Plastic.
  •  
5.
  • Adams, Robin, 1978, et al. (författare)
  • A Type Theory for Probabilistic and Bayesian Reasoning
  • 2018
  • Ingår i: Leibniz International Proceedings in Informatics (LIPIcs). - 1868-8969. - 9783959770309 ; 69, s. 11-134
  • Konferensbidrag (refereegranskat)abstract
    • This paper introduces a novel type theory and logic for probabilistic reasoning. Its logic is quantitative, with fuzzy predicates. It includes normalisation and conditioning of states. This conditioning uses a key aspect that distinguishes our probabilistic type theory from quantum type theory, namely the bijective correspondence between predicates and side-effect free actions (called instrument, or assert, maps). The paper shows how suitable computation rules can be derived from this predicate-action correspondence, and uses these rules for calculating conditional probabilities in two well-known examples of Bayesian reasoning in (graphical) models. Our type theory may thus form the basis for a mechanisation of Bayesian inference.
  •  
6.
  • Adams, Robin, 1978, et al. (författare)
  • Classical Predicative Logic-Enriched Type Theories
  • 2010
  • Ingår i: Annals of Pure and Applied Logic. - : Elsevier BV. - 0168-0072. ; 161:11, s. 1315-1345
  • Tidskriftsartikel (refereegranskat)abstract
    • A logic-enriched type theory (LTT) is a type theory extended with a primitive mechanism for forming and proving propositions. We construct two LTTs, named LTT0 and LTT0*, which we claim correspond closely to the classical predicative systems of second order arithmetic ACA0 and ACA0*. We justify this claim by translating each second order system into the corresponding LTT, and proving that these translations are conservative. This is part of an ongoing research project to investigate how LTTs may be used to formalise different approaches to the foundations of mathematics. The two LTTs we construct are subsystems of the logic-enriched type theory LTTW, which is intended to formalise the classical predicative foundation presented by Herman Weyl in his monograph Das Kontinuum. The system has also been claimed to correspond to Weyl’s foundation. By casting ACA0 and ACA as LTTs, we are able to compare them with LTTW. It is a consequence of the work in this paper that LTTW is strictly stronger than ACA0. The conservativity proof makes use of a novel technique for proving one LTT conservative over another, involving defining an interpretation of the stronger system out of the expressions of the weaker. This technique should be applicable in a wide variety of different cases outside the present work.
  •  
7.
  • Adams, Robin, 1978 (författare)
  • Coercive subtyping in lambda-free logical frameworks
  • 2009
  • Konferensbidrag (refereegranskat)abstract
    • We show how coercive subtyping may be added to a lambda-free logical framework, by constructing the logical framework TF<, an extension of the lambda-free logical framework TF with coercive subtyping. Instead of coercive application, TF< makes use of a typecasting operation. We develop the metatheory of the resulting framework, including providing some general conditions under which typecasting in an object theory with coercive subtyping is decidable. We show how TF< may be embedded in the logical framework LF, and hence how results about LF may be deduced from results about TF< .
  •  
8.
  • Adams, Robin, 1978, et al. (författare)
  • Constructing Independently Verifiable Privacy-Compliant Type Systems for Message Passing between Black-Box Components
  • 2018
  • Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. ; 11294, s. 196-214
  • Konferensbidrag (refereegranskat)abstract
    • Privacy by design (PbD) is the principle that privacy should be considered at every stage of the software engineering process. It is increasingly both viewed as best practice and required by law. It is therefore desirable to have formal methods that provide guarantees that certain privacy-relevant properties hold. We propose an approach that can be used to design a privacy-compliant architecture without needing to know the source code or internal structure of any individual component. We model an architecture as a set of agents or components that pass messages to each other. We present in this paper algorithms that take as input an architecture and a set of privacy constraints, and output an extension of the original architecture that satisfies the privacy constraints.
  •  
9.
  • Adams, Robin, 1978 (författare)
  • Formalized metatheory with terms represented by an indexed family of types
  • 2006
  • Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Berlin, Heidelberg : Springer Berlin Heidelberg. - 1611-3349 .- 0302-9743. ; 3839, s. 1-16
  • Konferensbidrag (refereegranskat)abstract
    • It is possible to represent the terms of a syntax with binding constructors by a family of types, indexed by the free variables that may occur. This approach has been used several times for the study of syntax and substitution, but never for the formalization of the metatheory of a typing system. We describe a recent formalization of the metatheory of Pure Type Systems in Coq as an example of such a formalization. In general, careful thought is required as to how each definition and theorem should be stated, usually in an unfamiliar ‘big-step’ form; but, once the correct form has been found, the proofs are very elegant and direct.
  •  
10.
  •  
Skapa referenser, mejla, bekava och länka
  • Resultat 1-10 av 32
Typ av publikation
tidskriftsartikel (17)
konferensbidrag (10)
rapport (2)
forskningsöversikt (2)
annan publikation (1)
Typ av innehåll
refereegranskat (29)
övrigt vetenskapligt/konstnärligt (3)
Författare/redaktör
Adams, Robin, 1978 (15)
Luo, Zhaohui (4)
Schupp, Sibylle, 196 ... (3)
Adams, Robin (3)
Fincher, Sally (3)
Deloukas, Panos (3)
visa fler...
Handelsman, David J (2)
Hankey, Graeme J. (2)
Karlsson, Magnus (2)
Salomaa, Veikko (2)
Adams, Jenna N. (2)
Berron, David (2)
Börstler, Jürgen (2)
Pears, Arnold (2)
Boustedt, Jonas (2)
Dalenius, Peter (2)
Eken, Gunilla (2)
Heyer, Tim (2)
Jacobsson, Andreas (2)
Lindberg, Vanja (2)
Molin, Bengt (2)
Moström, Jan-Erik (2)
Wiggberg, Mattias (2)
Sattar, Naveed (2)
Ohlsson, Claes, 1965 (2)
Franks, Paul W. (2)
Wareham, Nicholas J. (2)
O'Neill, Terence W. (2)
Antonio, Leen (2)
Vanderschueren, Dirk (2)
Wu, Frederick C W (2)
Kuusisto, Johanna (2)
Laakso, Markku (2)
McCarthy, Mark I (2)
Wang, Lei (2)
Bork-Jensen, Jette (2)
Linneberg, Allan (2)
Grarup, Niels (2)
Pedersen, Oluf (2)
Hansen, Torben (2)
Langenberg, Claudia (2)
Boehnke, Michael (2)
Mohlke, Karen L (2)
Saleheen, Danish (2)
Thorleifsson, Gudmar (2)
Thorsteinsdottir, Un ... (2)
Stefansson, Kari (2)
Rotter, Jerome I. (2)
Mellström, Dan, 1945 (2)
Peters, Annette (2)
visa färre...
Lärosäte
Chalmers tekniska högskola (16)
Lunds universitet (7)
Göteborgs universitet (4)
Uppsala universitet (3)
Stockholms universitet (3)
Umeå universitet (2)
visa fler...
Högskolan i Gävle (1)
Karlstads universitet (1)
Karolinska Institutet (1)
Blekinge Tekniska Högskola (1)
Sveriges Lantbruksuniversitet (1)
visa färre...
Språk
Engelska (32)
Forskningsämne (UKÄ/SCB)
Naturvetenskap (24)
Medicin och hälsovetenskap (10)
Samhällsvetenskap (5)
Teknik (3)

År

Kungliga biblioteket hanterar dina personuppgifter i enlighet med EU:s dataskyddsförordning (2018), GDPR. Läs mer om hur det funkar här.
Så här hanterar KB dina uppgifter vid användning av denna tjänst.

 
pil uppåt Stäng

Kopiera och spara länken för att återkomma till aktuell vy