dataesr/scientific-paragraphs-categorization huggingface dataset:
For these reasons, we think that the FoCaLiZe  [10]  F-IDE is a good candidate to teach both computer science and discrete mathematics at the undergraduate level. Indeed, FoCaLiZe is an object-oriented programming environment that combines specifications, programs and proofs in the same language, and permits declarative proof descriptions inspired by Lamport's work  [14, 6]. These features can be used to formally express specifications and to develop the design and implementation of software as well as some hierarchy of mathematical structures, while proving that implementations (i. e. definitions) meet their specifications or design requirements (i. e. the properties that they are supposed to satisfy). Moreover, the object-oriented features of this language enable the development of an implementation by iterative refinement of its specification: many software components implemented can be built by inheritance and parameterization from already defined components.
Specification of binary relations In FoCaLiZe, the primitive entity of a development is the species. Species are the nodes of the hierarchy of structures that makes up a development. A species can be seen as a set of "things", called methods, related to the same concept. As in most modular design systems (i. e. object-oriented, abstract data types, etc. ) the idea is to group a data structure with the operations on the data structure, the specification of these operations (in the form of properties), the representation requirements, and the proofs of the properties. Therefore there are three kinds of methods: the carrier type, the programming methods which are functions and the logical methods which are statements, called here properties, and proofs. Each method is identified by its name and can be either declared (primitive constants, operations and properties) or defined (implementation of operations, proofs of theorems).
The method is contained spec corresponds to a logical method. Such methods represent the properties of programming methods. The declaration of a logical method is simply the statement of a property, while the definition is a proof of this statement. In the first case, we speak of properties (property) that are still to be proved later in the development, while in the second case we speak of theorems (theorem). The language also permits logical definitions (logical let) to bind names to logical statements. The language used for the statements is composed of the basic logical connectors \/, /\, ->, <->, not, and universal (all) and existential (ex) quantification over a FoCaLiZe type. As we can see in our example, as usual during a formal development (and as required as a good practice when applying formal methods), specifications are provided before implementations.
methods empty (for the empty part) and release (that permits to remove an element from a finite part). At this abstract level, these methods are only declared together with their specifications. Furthermore, we declare a method from list that aims at building a finite part from elements belonging to a list and which is used to specify the method belong. We can now refine species by representing finite parts with the concrete FoCaLiZe type list of lists. Within FoCaLiZe, the language used for the programming methods is similar to the functional core of OCaml (let-binding, pattern matching, conditional, higher order functions, etc), with the addition of a construction to call a method from a given structure. Thanks to these constructions, we can introduce the species Finite_parts_by_lists inheriting from Finite_parts and providing definitions for the programming methods.
Conclusion Using a computer to teach discrete mathematics at the undergraduate level is usally done by considering functionnal programming languages allowing students to formally express computational contents of mathematical concepts by programs and to informally reason on these programs. In this paper, we go one step futher by showing that abstract specifications and proofs can also be implemented at this level whitout assuming some advanced theoretical background. Indeed, while teaching experiences using F-IDE are mostly done at master level, we believe that such approaches can also be adopted for beginning Figure  1 : Formal development within FoCaLiZe students. We claim here that teaching how to develop software with F-IDE to beginners is essential to ease and to promote their use in industry.
FoCaLiZe was conceived from the beginning to help building systems with high safety and security assurances. FoCaLiZe includes a language based on firm theoretical results  [20] , with a clear semantics and provides an efficient implementation -via translation to OCaml. It has functional and object-oriented features and provides means for the programmers to write formal proofs of their code in a more or less detailed way within a declarative proof language based on the Zenon automatic theorem prover  [2]. Zenon eases the task of writing formal proofs and translates them into Coq for high-assurance checking. FoCaLiZe also provides powerful features (such as inheritance, parameterization and late-binding) that enable a stepwise refinement methodology to go from specification all the way down to executable code.
Indeed, thanks to the main features of FoCaLiZe, a formal development can be organized as a hierarchy (as illustrated in figure  1 ) which may have several roots: the upper levels of the hierarchy are built during the specification stage while the lower ones correspond to implementations. Thus, FoCaLiZe unifies within the same language the formal modeling work, the development of the code, and the certification proofs. Very important is the ability in FoCaLiZe to have specifications, implementations and proofs within the same language, since it eliminates the errors introduced between layers, at each switch between languages, during the development cycle. Other frameworks, like Atelier B  [1] , also aims at implementing tools for making formal development a reality. FoCaLiZe doesn't follow the same path, trying to keep the means of expression close to what engineers usually know: a programming language.
Of course, nowadays, proof assistants also provide some features for structuring code (module systems, type classes, etc), but most of them still cannot be used to obtain efficient programs. Compilation of FoCaLiZe developments leads to efficient OCaml programs (which are not obtained by extracting computational contents of proofs). It is this focus on efficiency that makes FoCaLiZe a real programming language. To our knowledge, only the Agda  [4]  programming language, based on dependent types and compiling via Haskell, has a comparable mix of features. Note that the FoCaLiZe language is also based on a dependent type language, but with some restrictions on dependencies. Furthermore, FoCaLiZe provides several automatic tools to ease the generation of programs from specifications, the generation of documentation, and the production of test suites  [5].
For all these reasons, we think that FoCaLiZe is not only well suited to develop critical systems but is also a good framework to teach both computer science and discrete mathematics courses. For example, we have already used  [8]  FoCaLiZe (together with Coq) to teach (at a master level) semantics of objectoriented features of programming languages. In this paper, we consider FoCaLiZe as a teaching tool at the undergraduate level and illustrate our approach with a small development introducing very basic concepts of discrete mathematics and showing how to mix both formal methods and discrete mathematics courses. Indeed, FoCaLiZe provides an environment simple enough to be usable by most students at university (even if they are not fully acquainted with theoretical concepts such as higher-order logics), in particular by making development of correct proofs as easy as possible and as readable as possible.
Moreover, FoCaLiZe leads to stress the process of abstraction through the construction, step by step, of problem solutions from their specifications. This can be helpful to improve the learning process of discrete mathematics but also to show to students that computer science involves a lot of mathematical activities and vice versa. In addition to pedagogical benefits, we believe that teaching how to use F-IDE as early as possible leads to raise the level of mathematical rigor for computer science so as to ensure that formal methods are perceived as valid professional disciplines by students. Formal methods will be of increasing value in computer and software engineering (especially for safety-critical, security-sensitive, and embedded systems) and we think that education is one challenge to take up in order to promote the dissemination of formal methods in software industry.
Cis-regulatory modules (CRMs) and motifs play a central role in tissue and condition-specific gene expression. Here we present Imogene, an ensemble of statistical tools that we have developed to facilitate their identification and implemented in a publicly available software. Starting from a small training set of mammalian or fly CRMs that drive similar gene expression profiles, Imogene determines de novo cis-regulatory motifs that underlie this coexpression. It can then predict on a genome-wide scale other CRMs with a regulatory potential similar to the training set. Imogene bypasses the need of large datasets for statistical analyses by making central use of the information provided by the sequenced genomes of multiple species, based on the developed statistical tools and explicit models for transcription factor binding site evolution.
The task of determining cis-regulatory elements is even more difficult for mammalian genomes than for Drosophila ones since they are an order of magnitude richer in intergenic sequences  (15, 16). To tackle this challenge, we have developed Imogene, a computer algorithm and software that we present here and characterize. Imogene predicts: (1) cis-regulatory sequences (of about 10 nt long) within a moderate set size of 10-30 CRMs, responsible for specific gene co-regulation, as well as a set of probability weight matrices (PWMs) or motifs  (17, 18)  characterizing the DNA-binding specificity of the associated putative factors. (2)  novel CRMs at the genomic scale with the same expression pattern as the starting set of CRMs, based on the set of built PWMs. Numerous algorithms have already been developed to try and map cis-underlying transcriptional regulation (see, e.
g. (3, 17, (19) (20) (21)  for recent reviews). Imogene differs from previ-ous methods in several respects. Imogene aim is most similar to the goal of the 'motif-blind' algorithms analyzed in  (22). These algorithms have been specially designed to characterize the specificity of a small set of CRMs, contrary to other algorithms that are aimed at the analysis of large datasets such as whole ChIP-seq peak regions  (23). As Imogene, they work de novo instead of using already characterized binding motifs  (24) (25) (26) (27) (28) (29) (30) (31) (32). Faced to the weak statistical discriminative power offered by the starting set of characterized CRMs, the algorithms of  (22)  try and distinguish regulatory sequences by their entire content in short nucleotide sequences as also proposed in other works  (33) (34) (35) (36) (37).
Genome alignments The alignments were downloaded from ftp://ftp. ensembl. org/pub/release-63/emf/ensembl-compara/ epo 12 eutherian for mammals and from http: //www. biostat. wisc. edu/ cdewey/fly CAF1/data for Drosophilae. For the latter case, we have used the alignments engineered by A. Caspi with the help of the Mercator and MAVID programs. In both cases, the alignments were processed through a customized script to produce alignments in FASTA format, mask for coding sequences (CDS) and simple repeats (see below). These scripts are available in the Imogene distribution.
Annotations The CDS coordinates were downloaded from ftp://ftp. ensembl. org/pub/release-64/gtf/mus musculus for mammals (mm9 coordinates) and from ftp: //ftp. flybase. net/releases/FB2011 06/dmel r5. 38/gff for Drosophilae (release 5 coordinates). In the case of mammals, the TSS coordinates were obtained separately from http: //hgdownload. cse. ucsc. edu/goldenPath/mm9/database. Mammalian alignments were already masked for repeat sequences. Drosophilae alignments were masked using the coordinates indicated in the gff file.
Training sets The two used mammalian training sets (limb and neural tube) were obtained from http://enhancer. lbl. gov based on the work of Visel et al. (11). They were manually curated to produce a high-quality dataset, with respectively 41 CRMs for the limb and 33 for the neural tube. We further pruned out uninformative CRMs for which no motifs could be generated, either because of repeat masking or because of lack of conservation. More precisely, the reference species sequence was scanned using a window size corresponding to the motif size. If a sequence did not contain any masked nucleotide, we looked in the other species for any unmasked sequence in the surrounding neighborhood of ±20 nt, our flexibility criterion when defining a conserved instance. If putative orthologous sequences were found in enough species to satisfy our conservation requirements (see below), the site was declared as a putative conserved site for a regulatory motif.
Main program The main program is written in C++ and adapted from the program used in a previous study  (14). It is distributed under the GNU GPL license and available as a git repository at http://github. com/hrouault/Imogene. The user manual is available at http://hrouault. github. io/Imogene/. The program can be accessed through a web interface at http: //mobyle. pasteur. fr/cgi-bin/portal. py#forms::imogene.
Binding site scores A given motif is represented by a PWM with frequency w i, b for the base b at position i. The index i runs from 1 to l m , the size of the motif, which is a parameter in the program that takes the same value for all considered motifs. The binding score of a sequence s i for such a motif is defined through the corresponding PWM as: S = i log 2 w i,s i π s i , ( 1 ) where b is the mean frequency of the base b within intergenic regions (π A,T = 0. 30 and π C,G = 0. 20) as measured on the 'background sequences' (see the 'Background sequences' subsection for their detailed description). A sequence is considered as a binding site in the reference species (D. melanogaster or Mus musculus) when its score S is larger than the score threshold (S s or S g ) defined by the user of Imogene.
Comparison with Kantorovitz et al. The data provided by Kantorovitz et al. (22)  consisted of eight classes of human CRMs, each class containing between 10 and 67 CRMs, with an average of 30 CRMs per class. Coordinates of the human CRMs were obtained from http://enhancer. lbl. gov and were converted from the human hg19 to the mouse mm9 assembly using the UCSC LiftOver tool, yielding a loss of 5-10 unmapped CRMs per class. The extraction of the mammalian alignments with Imogene resulted in another loss of 1-2 CRMs per class for which no alignment could be retrieved. Overall, the ratio of finally retrieved over initially available number of CRMs per class was the following: dorsal root ganglion (7/10), eye (12/16), forebrain (50/67), heart (9/19), hindbrain rhombencephalon (25/32), limb (24/35), midbrain mesencephalon (36/42) and neural tube (20/23).
Motifs identification In order to identify the known TFs that might correspond to the de novo generated motifs, we used the TRANSFAC  (48)  and JASPAR  (49)  databases, as well as the list of motifs provided in (50) from HT-Selex experiments and the UniPROBE database (51) created from protein binding array data. In order to avoid uninformative matches, we kept motifs that had an information content greater than 8 bits, a threshold approximately corresponding to four conserved nucleotides. This led us to keep 764 vertebrate motifs (934 total minus 170 below threshold) in the TRANSFAC database, 389 vertebrate motifs (476 total minus 87 below threshold) in the JASPAR database 575 HT-Selex motifs (580 total minus 5 below threshold) and 488 in the UniPROBE database (538 total minus 50 below threshold).
The larger the statistical deviation between the two distributions, the larger the PWM score and the more meaningful the PWM is deemed (see 'Ranking motifs' in the Materials and Methods section). In a final step, PWMs in the ranked list are compared (see 'Distance between motifs' in the Materials and Methods section) and, among similar ones, only the highest scoring one is kept. Although the identity of the TFs corresponding to the different PWMs of interest is not directly assessable by the algorithm, the comparison between the produced PWMs and existing databases can provide relevant information on their identity, as will be shown in the following sections. In its second mode, Scangen, Imogene determines intergenic sequences in the reference genome that are considered as putative CRMs with the same functional specificity as the training set.
g. Oct/Pou TF family and NeuroD motif in the neural CRMs). The motif content of each CRM is also provided in Supplementary Figures  S5  and S6. It is seen that the 10 best motifs appear on most CRMs of the training set. Among the existing algorithms, Kantorovitz et al. (22)  concluded that 'motif-blind' methods were the most successful for characterizing the specificity of a small set of CRMs. In order to further assess Imogene, we thus chose to compare its performance to that of these algorithms. Kantorovitz et al. (22)  benchmarked the prediction of the algorithms they examined on eight mammalian CRM datasets promoting expression in diverse tissues. We quantified the ability of Imogene to characterize these different sets of CRMs using the cross-validation protocol of  (22)  in which the CRMs to be tested were compared to intergenic sequences with similar GC content (see the Materials and Methods section).
Conservation and phylogeny were used for the generation of motifs (i. e. in Imogene Genmot mode). The CRM scoring was performed both using conservation, the normal Scangen operating mode, and without it in order to provide a fair comparison between Imogene and the 'motif-blind' methods that do not take advantage of conservation. The results are displayed in Figure  2  for the neural tube and limb CRM datasets and in Supplementary Figure  S7  for the other CRM datasets. In all cases, Imogene is found to perform comparably to the 'motif-blind' methods  (22). Without conservation, it appears nonetheless less efficient than the best 'motif-blind' methods, such as 'HexMCD'. The use of conservation significantly enhances Imogene predicting power and actually makes it the top predictor for several datasets (5/8).
2. The results are shown in Figure  3. We focus on the results obtained with the HB evolutionary model. Results (motifs and thresholds) are very comparable with the Felsenstein model. Motifs are shown on the right of the ROC plots and were generated on the positive classes with optimal parameters. The two classes were optimally discriminated using only two motifs in each class, with specificities S g = 11, S s = 8, comparable to that found in the learning task of the previous section. The closest motifs in the TRANSFAC (48) and JASPAR databases  (49) , as well as in the HT-Selex experiment list  (50)  and UniPROBE database  (51) , are shown in Supplementary Figure  S8. The best ranking motif of the neural CRMs is found to be unequivocally associated with the TRANSFAC Oct/Pou Transcription Factor known to be involved in the neural tube formation  (54).
Web interface The ensemble of developed statistical tools and the allied computer codes are freely available at http://github. com/ hrouault/Imogene. In addition, they can be used through a user-friendly web interface (http://mobyle. pasteur. fr/ cgi-bin/portal. py#forms::imogene) that provides motif and CRM predictions for the community. This interface is pow- ered by the Pasteur Institute Internet server through the mobyle framework  (55). The input web page and an example output web page are shown in Figures  5  and 6  respectively.
DISCUSSION We have presented Imogene, a set of statistical tools and a computer software able to predict de novo relevant motifs in a moderate size set of functionally related CRMs and able to infer novel CRMs with a low FPR in both Drosophilae and mammalian genomes. In contrast to methods dedicated to the general discovery of CRMs (see 2156 for recent reviews and assessment), the task requires to extract specific information from a training set that by itself offers only weak statistically discriminative power. This challenge was previously tackled by 'motif-blind' methods  (22)  that aimed to characterize the statistical distribution of short sequences in the training without providing information on specific TFBS. Imogene makes use of a different strategy to work efficiently from a CRM set of modest size.
Furthermore, the created PWMs appear to comprise both known and new motifs, in strong analogy with the previous studied cases in the fly. There are currently numerous cases for which a small number of CRMs belonging to the same program of gene expression has been characterized. At the same time, a large number of PWMs remain to be found. This is even more the case for CRMs. Therefore, the use of Imogene with its de novo motif building ability and allied CRM identification should provide helpful service to the community. We have further shown that Imogene can discriminate between classes of CRMs, a capability that is clearly distinct from general CRM prediction  (56). In this task, Imogene should usefully complement ChIP-seq data that are currently obtained for many developmental programs. Whereas ChIP-seq provides information on the binding of already known factors, Imogene is able to propose new motifs and helps to identify new involved DNA-binding cofactors and their binding sites.
We anticipate that Imogene CRM discriminative ability is likely to be important for future studies of transcription regulation specificity in closely related cell types (e. g. different neuronal cell types) since even large-scale studies will probably not provide more than a few tens of differentially activated CRMs, the training set size targeted by Imogene. We thus believe that Imogene is a useful addition to existing algorithms and softwares  (32). We hope that it will serve as a helpful and timely tool in the difficult deciphering of gene regulation in higher eukaryotes.
ACKNOWLEDGMENTS We wish to thank  I. Leroux ,  S. Meilhac  and  B. Robert  who helped us to characterize the patterns of expression of the mammalian CRMs used in the present work and  S. Eddy  for his critical reading of the manuscript. We are also grateful to  S. Sinha  for sending us the precise benchmark used in Kantorovitz et al. (22). We acknowledge the  Centre d'Informatique pour la Biologie at the Pasteur Institute  for its help in the design of a mobyle front-end to Imogene.
The neutrino energy spectra at production In this section we discuss the computation of the neutrino fluxes emerging from the DM annihilation process. Neutrinos are produced at several stages of the hadronic and leptonic cascades originating from the primary particles produced by annihilations, and these cascades develop within the dense matter of the astronomical body (the Sun). Such an environment has important consequences in determining the spectra. For example, some byproducts of the cascade can be absorbed by the surrounding matter; some others will be just 'slowed down'; others are negligibly affected. It is therefore important to model in the best possible way all these effects. We adopted and compared two strategies: 1) As described in section 3. 1. 1, we modified the public MonteCarlo code PYTHIA to include the effects of cascading energy losses with matter and absorption.