dataesr/scientific-paragraphs-categorization huggingface dataset:
Abbreviations AIDS: Acquired immunodeficiency syndrome; AMBER: Assisted model building with energy refinement; AMP: Adenosine monophosphate; ASFE: Advanced solvation force extrapolation; cAMP: Cyclic adenosine monophosphate; CF: Cystic fibrosis; COPASI: Complex pathway simulator; DFT: Density functional theory; DNA: Deoxyribonucleic acid; DTI: Diffusion tensor imaging; EC: Endothelial cell; ECM: Extracellular matrix; EOM: Equations of motion; EVB: Empirical valence bond; GAMESS: General atomic and molecular electronic structure system; GB: Generalized born; GF: Growth factor; GFP: Green fluorescent protein; GPCR: G protein-coupled receptor; GPU: Graphical processing unit; GROMOS: Groningen molecular simulation; HNC: Hypernetted chain; LJ: Lennard-Jones; LRC: Long-range van der Waals correction; MARTINI: Coarse-grained force field; MD: Molecular dynamics; MM: Molecular mechanics; MM-GBSA: Molecular mechanics Generalized Born surface area; MM-PBSA: Molecular mechanics Poisson-Boltzmann surface area; MRI: Magnetic resonance imaging; MTS: Multiple time step; MTS-MD: Multiple time step molecular dynamics; NAMD: Not just another molecular dynamics software; NMR: Nuclear magnetic resonance; ODE: Ordinary differential equation; OIN: Optimized isokinetic Nosé-Hoover chain; ONIOM: Our own N-layered Integrated molecular Orbital and molecular Mechanics; OPLS: Optimized Potentials for Liquid Simulations; P450: Cytochrome P450 superfamily of monooxygenases; PB: Poisson-Boltzmann; PDB: Protein data bank; PDE: Partial differential equation; PME: Particle mesh Ewald; PMF: Potential mean force; QM: Quantum mechanics; QM/ MM: Quantum mechanics/molecular mechanics; QSAR: Quantitative structure-activity relationship; REMD: Replica-exchange molecular dynamics; RISM: Reference interaction site model; RMSD: Root-mean-square deviation; RNA: Ribonucleic acid; SBML: Systems biology markup language; SBW: Systems biology workbench; SEIR: Susceptible-infected-exposed-recovered.
Abbreviations Abbreviations AIDS: Acquired immunodeficiency syndrome; AMBER: Assisted model building with energy refinement; AMP: Adenosine monophosphate; ASFE: Advanced solvation force extrapolation; cAMP: Cyclic adenosine monophosphate; CF: Cystic fibrosis; COPASI: Complex pathway simulator; DFT: Density functional theory; DNA: Deoxyribonucleic acid; DTI: Diffusion tensor imaging; EC: Endothelial cell; ECM: Extracellular matrix; EOM: Equations of motion; EVB: Empirical valence bond; GAMESS: General atomic and molecular electronic structure system; GB: Generalized born; GF: Growth factor; GFP: Green fluorescent protein; GPCR: G protein-coupled receptor; GPU: Graphical processing unit; GROMOS: Groningen molecular simulation; HNC: Hypernetted chain; LJ: Lennard-Jones; LRC: Long-range van der Waals correction; MARTINI: Coarse-grained force field; MD: Molecular dynamics; MM: Molecular mechanics; MM-GBSA: Molecular mechanics Generalized Born surface area; MM-PBSA: Molecular mechanics Poisson-Boltzmann surface area; MRI: Magnetic resonance imaging; MTS: Multiple time step; MTS-MD: Multiple time step molecular dynamics; NAMD: Not just another molecular dynamics software; NMR: Nuclear magnetic resonance; ODE: Ordinary differential equation; OIN: Optimized isokinetic Nosé-Hoover chain; ONIOM: Our own N-layered Integrated molecular Orbital and molecular Mechanics; OPLS: Optimized Potentials for Liquid Simulations; P450: Cytochrome P450 superfamily of monooxygenases; PB: Poisson-Boltzmann; PDB: Protein data bank; PDE: Partial differential equation; PME: Particle mesh Ewald; PMF: Potential mean force; QM: Quantum mechanics; QM/ MM: Quantum mechanics/molecular mechanics; QSAR: Quantitative structure-activity relationship; REMD: Replica-exchange molecular dynamics; RISM: Reference interaction site model; RMSD: Root-mean-square deviation; RNA: Ribonucleic acid; SBML: Systems biology markup language; SBW: Systems biology workbench; SEIR: Susceptible-infected-exposed-recovered.
Dependent types can be used to represent rich security policies in environments like databases and data-centric web applications where, for example, new classes of users and new kinds of data are encountered at run-time and the security level depends on the manipulated data itself  [23]. Such dependencies are not expressible in less expressive systems like MAC. Among other things, with dependent types, we can construct functions where the security level of the output depends on an argument: getPassword : (u : Username) -> Labeled u String Given a user name u, getPassword retrieves the corresponding password and classifies it at the security level of u. As such, we can express much more precise security policies that can depend on the manipulated data. Idris is a general-purpose functional programming language with fullspectrum dependent types, that is, there is no restrictions on which values may appear in types.
Notice that this proof may be constructed in the context of the sensitivity level l that we are declassifying from. The reason for parameterizing the predicate P by a data structure of type D is to allow declassification to be restricted to a specific context or data structure. This is used in the following example of an auction system, in which only the highest bid of a specific list of bids can be declassified. Example. Consider a two point lattice where L H, H L and an auction system where participants place bids secretly. All bids are labeled H and are put into a data structure BidLog. In the end, we want only the winning bid to be released and hence declassified to label L. To achieve this, we define a declassification predicate HighestBid. HighestBid : BidLog -> Bid -> Type HighestBid = \log, b => (Elem (label b) log, MaxBid b log) Informally, given a log log of labeled bids and a bid b, the predicate states that the bid is in the log, Elem (label b) log, and that it is the maximum bid, MaxBid b log.
Time-Based Hatches. To illustrate the idea of token hatches for the when dimension of declassification, consider the following example. Let Time be an abstract data type with a data constructor only available to trusted code and tick : DIO l Time a function that returns the current system time wrapped in the Time data type such that this is the only way for untrusted code to construct anything of type Time. Notice that this does not expose an unrestricted timer API as untrusted code can not inspect the actual value. Now, we instantiate the token hatch builder with a predicate that demands the existence of a Time token that is greater than some specific value. TimeHatch : Time -> Type TimeHatch t = (t' ** t <= t' = True) -> Labeled H Nat -> Labeled L Nat As such, TimeHatch t can only be used after a specific point in time t has passed as only then untrusted code will be able to satisfy the predicate.
Notice how assignment of authorities to pieces of code consequently is a part of the trusted code. Now, we instantiate the token hatch builder with a predicate that demands the authority of s to declassify information at that level. That is, authHatch makes it possible to declassify information at level l to l' given an instance of the Authority l data type. Example. Consider the scenario of an online dating service that has the distinguishing feature of allowing its users to specify the visibility of their profiles at a fine-grained level. To achieve this, the service allows users to provide a discovery agent that controls their visibility. Consider a user, Bob, whose implementation of the discovery agent takes as input his own profile and the profile of another user, say Alice. The agent returns a possibly side-effectful computation that returns an option type indicating whether Bob wants to be discovered by Alice.
Introduction Vulnerabilities that compromise memory safety are at the heart of many attacks. Spatial safety, one aspect of memory safety, is ensured when any pointer dereference is always within the memory allocated to that pointer. Buffer overruns violate spatial safety, and still constitute a common cause of vulnerability. During 2012-2018, buffer overruns were the source of 9. 7% to 18. 4% of CVEs reported in the NIST vulnerability database  [27] , constituting the leading single cause of CVEs. The source of memory unsafety starts with the language definitions of C and C++, which render out-of-bounds pointer dereferences "undefined. " Traditional compilers assume they never happen. Many efforts over the last 20 years have aimed for greater assurance by proving that accesses are in bounds, and/or preventing out-of-bounds accesses from happening via inserted dynamic checks  [1] [2] [3] [4] [5] [6] [7] [8] [9] [10] 12, 15, 16, 18, 22, 25, 26, 29].
Checked Code Cannot Be Blamed Our main formal result is that well-typed programs will never fail with a spatial safety violation that is due to a checked region of code, i. e. , checked code cannot be blamed. This section presents the main result and outlines its proof. We have mechanized the full proof using the Coq proof assistant. The development is roughly 3500 lines long, including comments. It is freely available at https:// github. com/plum-umd/checkedc/tree/master/coq.
Conclusions and Future Work This paper has presented CoreChkC, a core formalism for Checked C, an extension to C aiming to provide spatial safety. CoreChkC models Checked C's safe (checked) and unsafe (legacy) pointers; while these pointers can be intermixed, use of legacy pointers is severely restricted in checked regions of code. We prove that these restrictions are efficacious: checked code cannot be blamed in the sense that any spatial safety violation must be directly or indirectly due to an unsafe operation outside a checked region. Our formalization and proof are mechanized in the Coq proof assistant; this mechanization is available at https://github. com/plum-umd/checkedc/tree/master/coq. The freedom to intermix safe and legacy pointers in Checked C programs affords flexibility when porting legacy code.
We show this is true for automated porting as well. A whole-program rewriting algorithm we built is able to make more pointers safe than it would if pointer types were all-or-nothing; we do this by taking advantage of Checked C's allowed casts and interface types. The tool implementing this algorithm, checked-c-convert, is distributed with Checked C at https://github. com/Microsoft/checkedc-clang. As future work, we are interested in formalizing other aspects of Checked C, notably its subsumption algorithm and support for flow-sensitive typing (to handle pointer arithmetic), to prove that these aspects of the implementation are correct. We are also interested in expanding support for the rewriting algorithm, by using more advanced static analysis techniques to infer numeric bounds suitable for re-writing array types.
We formally prove that the optimized and unoptimized versions are equivalent, both functionally and w. r. t. privacy of parties' inputs. Our card dealing application relies on Wys 's support for secret shares  [57]. We formally prove that the card dealing algorithm always deals a fresh card. In sum, Wys constitutes the first DSL that supports proving security and correctness properties about MPC programs, which are executed by a partially verified implementation of a full-featured language. No prior DSL provides these benefits (Sect. 5). The Wys implementation, example programs, and proofs are publicly available on Github at https://github. com/FStarLang/FStar/tree/ stratified_last/examples/wysteria. 2.
Embedding a Type System for Wys in F Designing high-level, multi-party computations is relatively easy using Wysteria's abstractions. Before trying to run such a computation, we might wonder: 1. Is it realizable? For example, does a computation that is claimed to be executed only by some principals ps (e. g. , using an as_par ps or an as_sec ps) only ever access data belonging to ps? 2. Is it correct? For example, does median_opt correctly compute the median of Alice and Bob's inputs? 3. Is it secure? For example, do the optimizations in median_opt, which produce more visible outputs, potentially leak more about the inputs? By embedding Wys in F and leveraging its extensible, monadic, dependent type-and-effect system, we address each of these three questions. We define a new indexed monad called Wys for computations that use MPC combinators as_sec and as_par.
Deploying Wys Programs Having defined a proved-secure MPC program in Wys , how do we run it? Doing so requires the following steps (Fig. 1 ). First, we run the F compiler in a special mode that extracts the Wys code (say psi. fst), into the Wys AST as a data structure (in psi. ml). Except for the Wys specific nodes (as_sec, as_par, etc. ), the rest of the program is extracted into FFI nodes that indicate the use of, or calls into, functionality provided by F itself. The next step is for each party to run the extracted AST using the Wys interpreter. This interpreter is written in F and we have proved (see Sect. 3. 5) that it implements a deep embedding of the Wys semantics, also specified in F (Figs. 5  and 6 , Sect. 3). The interpreter is extracted to OCaml by the usual F extraction. Each party's interpreter executes the AST locally until it reaches an as_sec ps f node, where the interpreter's back-end compiles f, on-the-fly, for particular values of the secrets in f's environment, to a boolean circuit.
4 We explain how to combine this with d X -privacy which extends privacy for databases to other unstructured domains (such as texts). In Sect. 2 we set out the details of the bag-of-words representation of documents and define the Earth Mover's metric for topic classification. In Sect. 3 we define a generic mechanism which satisfies "E dX -privacy" relative to the Earth Mover's metric E dX and show how to use it for our obfuscation problem. We note that our generic mechanism is of independent interest for other domains where the Earth Mover's metric applies. In Sect. 4 we describe how to implement the mechanism for data represented as real-valued vectors and prove its privacy/utility properties with respect to the Earth Mover's metric; in Sect. 5 we show how this applies to bags-of-words. Finally in Sect.
Differential Privacy and the Earth Mover's Metric Differential Privacy was originally defined with the protection of individuals' data in mind. The intuition is that privacy is achieved through "plausible deniability", i. e. whatever output is obtained from a query, it could have just as easily have arisen from a database that does not contain an individual's details, as from one that does. In particular, there should be no easy way to distinguish between the two possibilities. Privacy in text processing means something a little different. A "query" corresponds to releasing the topic-related contents of the document (in our case the bag-of-words)-this relates to the utility because we would like to reveal the semantic content. The privacy relates to investing individual documents with plausible deniability, rather than individual authors directly.
" This is also the domain that was used in the PAN@Clef 2018 author attribution challenge,  11  although for this work we scraped our own dataset. We chose one of the largest fan fiction sites and the two largest "fandoms" there; 12  these fandoms are our topics. We scraped the stories from these fandoms, the largest proportion of which are for use in training our topic classification model. We held out two subsets of size 20 and 50, evenly split between fandoms/topics, for the evaluation of our privacy mechanism. 13 We follow the evaluation framework of  [28] : for each author we construct an known-author text and an unknown-author snippet that we have to match to an author on the basis of the known-author texts. (See Appendix in our complete paper  [15]  for more detail. ) Word Embeddings.
There are sets of word embeddings trained on large datasets that have been made publicly available. Most of these, however, are already normalised, which makes them unsuitable for our method. We therefore use the Google News word2vec embeddings as the only large-scale unnormalised embeddings available. (See Appendix in our complete paper  [15]  for more detail. ) Inference Mechanisms. We have two sorts of machine learning inference mechanisms: our adversary mechanism for author identification, and our utility-related mechanism for topic classification. For each of these, we can define inference mechanisms both within the same representational space or in a different representational space. As we noted above, in practice both author identification adversary and topic classification will use different representations, but examining same-representation inference mechanisms can give an insight into what is happening within that space.
For the 20-author set, a random guess baseline would give 1 correct author prediction, and 10 correct topic predictions; for the 50-author set, these values are 1 and 25 respectively. Performance on the unmodified snippets using different-representation inference mechanisms is quite good: author identification gets 15/20 correct for the 20-author set and 27/50 for the 50-author set; and topic classification 18/20 and 43/50 (comparable to the validation set accuracy, although slightly lower, which is to be expected given that the texts are much shorter). For various levels of , with our different-representation inference mechanisms we see broadly the behaviour we expected: the performance of author identification drops, while topic classification holds roughly constant. Author identification here does not drop to chance levels: we speculate that this is because (in spite of our choice of dataset for this purpose) there are still some topic clues that the algorithm of  [28]  takes advantage of: one author of Harry Potter fan fiction might prefer to write about a particular character (e.
Cumby and Ghani  [11]  proposed k-confusability, inspired by k-anonymity  [50] , to perturb sensitive terms in a document so that its (utility) class is confusable with at least k other classes. Their approach requires a complete dataset of similar documents for computing (mis)classification probabilities. Anandan et al. [3]  proposed t-plausibility which generalises sensitive terms such that any document could have been generated from at least t other documents. Sánchez and Batet  [45]  proposed C-sanitisation, a model for both detection and protection of sensitive terms (C) using information theoretic guarantees. In particular, a C-sanitised document should contain no collection of terms which can be used to infer any of the sensitive terms. Finally, there has been some work on noise-addition techniques in this area.
Phrases denotational operational Event Poset constrains Small-Step  Events are the foundation for both semantic notions depicted in Fig. 1. Each semantic notion constrains the event ordering in its own way. The denotational semantics of the left leg of the triangle is presented in Sect. 5, and the operational semantics of the right leg is given in Sect. 6. The crucial theorem connecting the two semantic notions is sketched in Sect. 7. All lemmas and theorems stated in this paper have been formally verified using the Coq proof assistant  [1]. The Coq proofs are available at https://kusldg. github. io/copland/. The notation used in this paper closely follows the Coq proofs. The tables in Appendix B link figures and formulas with their definitions in the Coq proofs. Before jumping into the formal details of the syntax and semantics of Copland, however, we present a sequence of simple examples designed to give the reader a feel for the language and its purpose.
Acknowledgements. We thank the anonymous reviewers for useful comments. This work was supported by  JSPS KAKENHI  Grant Numbers  17H01720  and  18K19787 ,  JSPS  Core-to- Core Program ,  A. Advanced Research Networks ,  JSPS Bilateral Collaboration Research, and Office of Naval Research (ONR)  award # N00014-17-1-2787. Acknowledgements. Thanks are due to  Mathias Vorreiter Pedersen ,  Bas Spitters ,  Alejandro Russo , and  Marco Vassena  for their valuable insights and the anonymous reviewers for their comments on this paper. This work is partially supported by  DFF  project  6108-00363  from The  Danish Council for Independent Research for the Natural Sciences (FNU) ,  Aarhus University Research Foundation , and the  Concordium Blockchain Research Center, Aarhus University, Denmark. Acknowledgments.
We would like to thank the anonymous reviewers for helpful comments on drafts of this paper, and  Sam Elliott  for contributions to the portions of the design and implementation of Checked C presented in this paper. This research was funded in part by the  U. S. National Science Foundation  under grants  CNS-1801545  and  EDU-1319147. Acknowledgments. We would like to thank the anonymous reviewers,  Catalin Hriţcu , and  Matthew Hammer  for helpful comments on drafts of this paper. This research was funded in part by the  U. S. National Science Foundation  under grants  CNS-1563722 ,  CNS-1314857 , and  CNS-1111599. Acknowledgements. We are grateful to  Andreas Lochbihler  for providing and continuing to develop CryptHOL and for his kind help given with using it. Acknowledgements. Massimo Bartoletti  is partially supported by Aut.
In: Conference on Timely Results in Operating Systems, Monterey, CS, US (2015) 66. Yang, E. Z. , Mazières, D. : Dynamic space limits for Haskell. In: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2014, pp. 588-598. ACM, New York (2014) 67. Yang, J. , Hance, T. , Austin, T. H. , Solar-Lezama, A. , Flanagan, C. , Chong, S. : Pre- cise, dynamic information flow for database-backed applications. ACM SIGPLAN Not. 51, 631-647 (2016) 68. Yang, J. , Yessenov, K. , Solar-Lezama, A. : A language for automatically enforcing privacy policies. ACM SIGPLAN Not. 47, 85-96 (2012) 69. Zeldovich, N. , Boyd-Wickizer, S. , Kohler, E. , Mazières, D. : Making information flow explicit in HiStar. In: Proceedings of the 7th Symposium on Operating Systems Design and Implementation, pp.
Automatic text summarization aims to produce summaries for one or more texts using machine techniques. In this paper, we propose a novel statistical summarization system for Arabic texts. Our system uses a clustering algorithm and an adapted discriminant analysis method: mRMR (minimum redundancy and maximum relevance) to score terms. Through mRMR analysis, terms are ranked according to their discriminant and coverage power. Second, we propose a novel sentence extraction algorithm which selects sentences with top ranked terms and maximum diversity. Our system uses minimal language-dependant processing: sentence splitting, tokenization and root extraction. Experimental results on EASC and TAC 2011 MultiLingual datasets showed that our proposed approach is competitive to the state of the art systems.
Cross-lingual and multilingual summarizations received considerable attention and made some interesting multilingual datasets available. The goal of text summarization is to produce a condensed version of one or more texts using computer techniques. This will help the reader to decide if a document contains needed information with minimum effort and time loss. Thus, a good summarizer should find key information and omit redundant information. For example, if we perform a search on a particular subject, such as ''Arabic text summarization", we will find a multitude of documents. Among them, some are very interesting, and others are less relevant. Sorting these documents is a tedious task, which will take significant time. Thus, tools such as single-and multi-document summarization systems are quite useful.