Search

Your search keyword '"Melquiond AS"' showing total 624 results
Start Over Author "Melquiond AS"
624 results on '"Melquiond AS"'

3. A strong call-by-need calculus

Author

Balabonski, Thibaut, Lanco, Antoine, and Melquiond, Guillaume

Subjects
Computer Science - Logic in Computer Science
Abstract

We present a call-by-need $\lambda$-calculus that enables strong reduction (that is, reduction inside the body of abstractions) and guarantees that arguments are only evaluated if needed and at most once. This calculus uses explicit substitutions and subsumes the existing strong-call-by-need strategy, but allows for more reduction sequences, and often shorter ones, while preserving the neededness. The calculus is shown to be normalizing in a strong sense: Whenever a $\lambda$-term t admits a normal form n in the $\lambda$-calculus, then any reduction sequence from t in the calculus eventually reaches a representative of the normal form n. We also exhibit a restriction of this calculus that has the diamond property and that only performs reduction sequences of minimal length, which makes it systematically better than the existing strategy. We have used the Abella proof assistant to formalize part of this calculus, and discuss how this experiment affected its design. In particular, it led us to derive a new description of call-by-need reduction based on inductive rules.

Published
2021
Full Text
View/download PDF

5. Plotting in a Formally Verified Way

Author

Melquiond, Guillaume

Subjects
Computer Science - Software Engineering, Computer Science - Logic in Computer Science
Abstract

An invaluable feature of computer algebra systems is their ability to plot the graph of functions. Unfortunately, when one is trying to design a library of mathematical functions, this feature often falls short, producing incorrect and potentially misleading plots, due to accuracy issues inherent to this use case. This paper investigates what it means for a plot to be correct and how to formally verify this property. The Coq proof assistant is then turned into a tool for plotting function graphs using reliable polynomial approximations. This feature is provided as part of the CoqInterval library., Comment: In Proceedings F-IDE 2021, arXiv:2108.02369

Published
2021
Full Text
View/download PDF

8. A strong call-by-need calculus

Author

Thibaut Balabonski, Antoine Lanco, and Guillaume Melquiond

Subjects
computer science - logic in computer science, Logic, BC1-199, Electronic computers. Computer science, QA75.5-76.95
Abstract

We present a call-by-need $\lambda$-calculus that enables strong reduction (that is, reduction inside the body of abstractions) and guarantees that arguments are only evaluated if needed and at most once. This calculus uses explicit substitutions and subsumes the existing strong-call-by-need strategy, but allows for more reduction sequences, and often shorter ones, while preserving the neededness. The calculus is shown to be normalizing in a strong sense: Whenever a $\lambda$-term t admits a normal form n in the $\lambda$-calculus, then any reduction sequence from t in the calculus eventually reaches a representative of the normal form n. We also exhibit a restriction of this calculus that has the diamond property and that only performs reduction sequences of minimal length, which makes it systematically better than the existing strategy. We have used the Abella proof assistant to formalize part of this calculus, and discuss how this experiment affected its design. In particular, it led us to derive a new description of call-by-need reduction based on inductive rules.

Published
2023
Full Text
View/download PDF

12. Robust detection of translocations in lymphoma FFPE samples using targeted locus capture-based sequencing

Author

Amin Allahyar, Mark Pieterse, Joost Swennenhuis, G. Tjitske Los-de Vries, Mehmet Yilmaz, Roos Leguit, Ruud W. J. Meijers, Robert van der Geize, Joost Vermaat, Arjen Cleven, Tom van Wezel, Arjan Diepstra, Léon C. van Kempen, Nathalie J. Hijmering, Phylicia Stathi, Milan Sharma, Adrien S. J. Melquiond, Paula J. P. de Vree, Marjon J. A. M. Verstegen, Peter H. L. Krijger, Karima Hajo, Marieke Simonis, Agata Rakszewska, Max van Min, Daphne de Jong, Bauke Ylstra, Harma Feitsma, Erik Splinter, and Wouter de Laat

Subjects
Science
Abstract

Preservation of cancer biopsies by FFPE introduces DNA fragmentation, hindering analysis of rearrangements. Here the authors introduce FFPE Targeted Locus Capture for identification of translocations in preserved samples.

Published
2021
Full Text
View/download PDF

14. Extending the Precision

Author

Muller, Jean-Michel, Brunie, Nicolas, de Dinechin, Florent, Jeannerod, Claude-Pierre, Joldes, Mioara, Lefèvre, Vincent, Melquiond, Guillaume, Revol, Nathalie, Torres, Serge, Muller, Jean-Michel, Brunie, Nicolas, de Dinechin, Florent, Jeannerod, Claude-Pierre, Joldes, Mioara, Lefèvre, Vincent, Melquiond, Guillaume, Revol, Nathalie, and Torres, Serge

Published
2018
Full Text
View/download PDF

15. Interval Arithmetic

Author

Muller, Jean-Michel, Brunie, Nicolas, de Dinechin, Florent, Jeannerod, Claude-Pierre, Joldes, Mioara, Lefèvre, Vincent, Melquiond, Guillaume, Revol, Nathalie, Torres, Serge, Muller, Jean-Michel, Brunie, Nicolas, de Dinechin, Florent, Jeannerod, Claude-Pierre, Joldes, Mioara, Lefèvre, Vincent, Melquiond, Guillaume, Revol, Nathalie, and Torres, Serge

Published
2018
Full Text
View/download PDF

16. Verifying Floating-Point Algorithms

Author

Muller, Jean-Michel, Brunie, Nicolas, de Dinechin, Florent, Jeannerod, Claude-Pierre, Joldes, Mioara, Lefèvre, Vincent, Melquiond, Guillaume, Revol, Nathalie, Torres, Serge, Muller, Jean-Michel, Brunie, Nicolas, de Dinechin, Florent, Jeannerod, Claude-Pierre, Joldes, Mioara, Lefèvre, Vincent, Melquiond, Guillaume, Revol, Nathalie, and Torres, Serge

Published
2018
Full Text
View/download PDF

17. Complex Numbers

Author

Muller, Jean-Michel, Brunie, Nicolas, de Dinechin, Florent, Jeannerod, Claude-Pierre, Joldes, Mioara, Lefèvre, Vincent, Melquiond, Guillaume, Revol, Nathalie, Torres, Serge, Muller, Jean-Michel, Brunie, Nicolas, de Dinechin, Florent, Jeannerod, Claude-Pierre, Joldes, Mioara, Lefèvre, Vincent, Melquiond, Guillaume, Revol, Nathalie, and Torres, Serge

Published
2018
Full Text
View/download PDF

18. Enhanced Floating-Point Sums, Dot Products, and Polynomial Values

Author

Muller, Jean-Michel, Brunie, Nicolas, de Dinechin, Florent, Jeannerod, Claude-Pierre, Joldes, Mioara, Lefèvre, Vincent, Melquiond, Guillaume, Revol, Nathalie, Torres, Serge, Muller, Jean-Michel, Brunie, Nicolas, de Dinechin, Florent, Jeannerod, Claude-Pierre, Joldes, Mioara, Lefèvre, Vincent, Melquiond, Guillaume, Revol, Nathalie, and Torres, Serge

Published
2018
Full Text
View/download PDF

19. Software Implementation of Floating-Point Arithmetic

Author

Muller, Jean-Michel, Brunie, Nicolas, de Dinechin, Florent, Jeannerod, Claude-Pierre, Joldes, Mioara, Lefèvre, Vincent, Melquiond, Guillaume, Revol, Nathalie, Torres, Serge, Muller, Jean-Michel, Brunie, Nicolas, de Dinechin, Florent, Jeannerod, Claude-Pierre, Joldes, Mioara, Lefèvre, Vincent, Melquiond, Guillaume, Revol, Nathalie, and Torres, Serge

Published
2018
Full Text
View/download PDF

20. Languages and Compilers

Author

Muller, Jean-Michel, Brunie, Nicolas, de Dinechin, Florent, Jeannerod, Claude-Pierre, Joldes, Mioara, Lefèvre, Vincent, Melquiond, Guillaume, Revol, Nathalie, Torres, Serge, Muller, Jean-Michel, Brunie, Nicolas, de Dinechin, Florent, Jeannerod, Claude-Pierre, Joldes, Mioara, Lefèvre, Vincent, Melquiond, Guillaume, Revol, Nathalie, and Torres, Serge

Published
2018
Full Text
View/download PDF

21. Algorithms for the Basic Operations

Author

Muller, Jean-Michel, Brunie, Nicolas, de Dinechin, Florent, Jeannerod, Claude-Pierre, Joldes, Mioara, Lefèvre, Vincent, Melquiond, Guillaume, Revol, Nathalie, Torres, Serge, Muller, Jean-Michel, Brunie, Nicolas, de Dinechin, Florent, Jeannerod, Claude-Pierre, Joldes, Mioara, Lefèvre, Vincent, Melquiond, Guillaume, Revol, Nathalie, and Torres, Serge

Published
2018
Full Text
View/download PDF

22. Evaluating Floating-Point Elementary Functions

Author

Muller, Jean-Michel, Brunie, Nicolas, de Dinechin, Florent, Jeannerod, Claude-Pierre, Joldes, Mioara, Lefèvre, Vincent, Melquiond, Guillaume, Revol, Nathalie, Torres, Serge, Muller, Jean-Michel, Brunie, Nicolas, de Dinechin, Florent, Jeannerod, Claude-Pierre, Joldes, Mioara, Lefèvre, Vincent, Melquiond, Guillaume, Revol, Nathalie, and Torres, Serge

Published
2018
Full Text
View/download PDF

23. Hardware Implementation of Floating-Point Arithmetic

Author

Muller, Jean-Michel, Brunie, Nicolas, de Dinechin, Florent, Jeannerod, Claude-Pierre, Joldes, Mioara, Lefèvre, Vincent, Melquiond, Guillaume, Revol, Nathalie, Torres, Serge, Muller, Jean-Michel, Brunie, Nicolas, de Dinechin, Florent, Jeannerod, Claude-Pierre, Joldes, Mioara, Lefèvre, Vincent, Melquiond, Guillaume, Revol, Nathalie, and Torres, Serge

Published
2018
Full Text
View/download PDF

24. Basic Properties and Algorithms

Author

Muller, Jean-Michel, Brunie, Nicolas, de Dinechin, Florent, Jeannerod, Claude-Pierre, Joldes, Mioara, Lefèvre, Vincent, Melquiond, Guillaume, Revol, Nathalie, Torres, Serge, Muller, Jean-Michel, Brunie, Nicolas, de Dinechin, Florent, Jeannerod, Claude-Pierre, Joldes, Mioara, Lefèvre, Vincent, Melquiond, Guillaume, Revol, Nathalie, and Torres, Serge

Published
2018
Full Text
View/download PDF

25. Floating-Point Formats and Environment

Author

Muller, Jean-Michel, Brunie, Nicolas, de Dinechin, Florent, Jeannerod, Claude-Pierre, Joldes, Mioara, Lefèvre, Vincent, Melquiond, Guillaume, Revol, Nathalie, Torres, Serge, Muller, Jean-Michel, Brunie, Nicolas, de Dinechin, Florent, Jeannerod, Claude-Pierre, Joldes, Mioara, Lefèvre, Vincent, Melquiond, Guillaume, Revol, Nathalie, and Torres, Serge

Published
2018
Full Text
View/download PDF

26. Definitions and Basic Notions

Author

Muller, Jean-Michel, Brunie, Nicolas, de Dinechin, Florent, Jeannerod, Claude-Pierre, Joldes, Mioara, Lefèvre, Vincent, Melquiond, Guillaume, Revol, Nathalie, Torres, Serge, Muller, Jean-Michel, Brunie, Nicolas, de Dinechin, Florent, Jeannerod, Claude-Pierre, Joldes, Mioara, Lefèvre, Vincent, Melquiond, Guillaume, Revol, Nathalie, and Torres, Serge

Published
2018
Full Text
View/download PDF

27. Introduction

Author

Muller, Jean-Michel, Brunie, Nicolas, de Dinechin, Florent, Jeannerod, Claude-Pierre, Joldes, Mioara, Lefèvre, Vincent, Melquiond, Guillaume, Revol, Nathalie, Torres, Serge, Muller, Jean-Michel, Brunie, Nicolas, de Dinechin, Florent, Jeannerod, Claude-Pierre, Joldes, Mioara, Lefèvre, Vincent, Melquiond, Guillaume, Revol, Nathalie, and Torres, Serge

Published
2018
Full Text
View/download PDF

29. Robust detection of translocations in lymphoma FFPE samples using targeted locus capture-based sequencing

Author

Allahyar, Amin, Pieterse, Mark, Swennenhuis, Joost, Los-de Vries, G. Tjitske, Yilmaz, Mehmet, Leguit, Roos, Meijers, Ruud W. J., van der Geize, Robert, Vermaat, Joost, Cleven, Arjen, van Wezel, Tom, Diepstra, Arjan, van Kempen, Léon C., Hijmering, Nathalie J., Stathi, Phylicia, Sharma, Milan, Melquiond, Adrien S. J., de Vree, Paula J. P., Verstegen, Marjon J. A. M., Krijger, Peter H. L., Hajo, Karima, Simonis, Marieke, Rakszewska, Agata, van Min, Max, de Jong, Daphne, Ylstra, Bauke, Feitsma, Harma, Splinter, Erik, and de Laat, Wouter

Published
2021
Full Text
View/download PDF

31. A Why3 Framework for Reflection Proofs and Its Application to GMP’s Algorithms

Author

Melquiond, Guillaume, Rieu-Helft, Raphaël, Hutchison, David, Series Editor, Kanade, Takeo, Series Editor, Kittler, Josef, Series Editor, Kleinberg, Jon M., Series Editor, Mattern, Friedemann, Series Editor, Mitchell, John C., Series Editor, Naor, Moni, Series Editor, Pandu Rangan, C., Series Editor, Steffen, Bernhard, Series Editor, Terzopoulos, Demetri, Series Editor, Tygar, Doug, Series Editor, Weikum, Gerhard, Series Editor, Galmiche, Didier, editor, Schulz, Stephan, editor, and Sebastiani, Roberto, editor

Published
2018
Full Text
View/download PDF

32. Trusting Computations: a Mechanized Proof from Partial Differential Equations to Actual Program

Author

Boldo, Sylvie, Clément, François, Filliâtre, Jean-Christophe, Mayero, Micaela, Melquiond, Guillaume, and Weis, Pierre

Subjects
Mathematics - Numerical Analysis, Computer Science - Logic in Computer Science
Abstract

Computer programs may go wrong due to exceptional behaviors, out-of-bound array accesses, or simply coding errors. Thus, they cannot be blindly trusted. Scientific computing programs make no exception in that respect, and even bring specific accuracy issues due to their massive use of floating-point computations. Yet, it is uncommon to guarantee their correctness. Indeed, we had to extend existing methods and tools for proving the correct behavior of programs to verify an existing numerical analysis program. This C program implements the second-order centered finite difference explicit scheme for solving the 1D wave equation. In fact, we have gone much further as we have mechanically verified the convergence of the numerical scheme in order to get a complete formal proof covering all aspects from partial differential equations to actual numerical results. To the best of our knowledge, this is the first time such a comprehensive proof is achieved., Comment: N° RR-8197 (2012). arXiv admin note: text overlap with arXiv:1112.1795

Published
2012

33. Wave Equation Numerical Resolution: a Comprehensive Mechanized Proof of a C Program

Author

Boldo, Sylvie, Clement, Francois, Filliâtre, Jean-Christophe, Mayero, Micaela, Melquiond, Guillaume, and Weis, Pierre

Subjects
Computer Science - Logic in Computer Science, Mathematics - Numerical Analysis
Abstract

We formally prove correct a C program that implements a numerical scheme for the resolution of the one-dimensional acoustic wave equation. Such an implementation introduces errors at several levels: the numerical scheme introduces method errors, and floating-point computations lead to round-off errors. We annotate this C program to specify both method error and round-off error. We use Frama-C to generate theorems that guarantee the soundness of the code. We discharge these theorems using SMT solvers, Gappa, and Coq. This involves a large Coq development to prove the adequacy of the C program to the numerical scheme and to bound errors. To our knowledge, this is the first time such a numerical analysis program is fully machine-checked., Comment: No. RR-7826 (2011)

Published
2011
Full Text
View/download PDF

34. Formal Proof of a Wave Equation Resolution Scheme: the Method Error

Author

Boldo, Sylvie, Clément, François, Filliâtre, Jean-Christophe, Mayero, Micaela, Melquiond, Guillaume, and Weis, Pierre

Subjects
Computer Science - Logic in Computer Science, Mathematics - Numerical Analysis
Abstract

Popular finite difference numerical schemes for the resolution of the one-dimensional acoustic wave equation are well-known to be convergent. We present a comprehensive formalization of the simplest one and formally prove its convergence in Coq. The main difficulties lie in the proper definition of asymptotic behaviors and the implicit way they are handled in the mathematical pen-and-paper proofs. To our knowledge, this is the first time such kind of mathematical proof is machine-checked., Comment: replaces arXiv:1001.4898

Published
2010
Full Text
View/download PDF

36. Certifying floating-point implementations using Gappa

Author

De Dinechin, Florent, Lauter, Christoph Quirin, and Melquiond, Guillaume

Subjects
Computer Science - Numerical Analysis, Computer Science - Mathematical Software
Abstract

High confidence in floating-point programs requires proving numerical properties of final and intermediate values. One may need to guarantee that a value stays within some range, or that the error relative to some ideal value is well bounded. Such work may require several lines of proof for each line of code, and will usually be broken by the smallest change to the code (e.g. for maintenance or optimization purpose). Certifying these programs by hand is therefore very tedious and error-prone. This article discusses the use of the Gappa proof assistant in this context. Gappa has two main advantages over previous approaches: Its input format is very close to the actual C code to validate, and it automates error evaluation and propagation using interval arithmetic. Besides, it can be used to incrementally prove complex mathematical properties pertaining to the C code. Yet it does not require any specific knowledge about automatic theorem proving, and thus is accessible to a wide community. Moreover, Gappa may generate a formal proof of the results that can be checked independently by a lower-level proof assistant like Coq, hence providing an even higher confidence in the certification of the numerical code. The article demonstrates the use of this tool on a real-size example, an elementary function with correctly rounded output.

Published
2008

37. Certification of bounds on expressions involving rounded operators

Author

Daumas, Marc and Melquiond, Guillaume

Subjects
Computer Science - Mathematical Software
Abstract

Gappa uses interval arithmetic to certify bounds on mathematical expressions that involve rounded as well as exact operators. Gappa generates a theorem with its proof for each bound treated. The proof can be checked with a higher order logic automatic proof checker, either Coq or HOL Light, and we have developed a large companion library of verified facts for Coq dealing with the addition, multiplication, division, and square root, in fixed- and floating-point arithmetics. Gappa uses multiple-precision dyadic fractions for the endpoints of intervals and performs forward error analysis on rounded operators when necessary. When asked, Gappa reports the best bounds it is able to reach for a given expression in a given context. This feature is used to quickly obtain coarse bounds. It can also be used to identify where the set of facts and automatic techniques implemented in Gappa becomes insufficient. Gappa handles seamlessly additional properties expressed as interval properties or rewriting rules in order to establish more intricate bounds. Recent work showed that Gappa is perfectly suited to the proof of correctness of small pieces of software. Proof obligations can be written by designers, produced by third-party tools or obtained by overloading arithmetic operators.

Published
2007

38. Floating-point arithmetic

Author

Sylvie Boldo, Claude-Pierre Jeannerod, Guillaume Melquiond, Jean-Michel Muller, Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Arithmétiques des ordinateurs, méthodes formelles, génération de code (ARIC), Laboratoire de l'Informatique du Parallélisme (LIP), École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Inria Lyon, Institut National de Recherche en Informatique et en Automatique (Inria), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), Centre National de la Recherche Scientifique (CNRS), ANR-20-CE48-0014,NuSCAP,Sûreté numérique pour les preuves assistées par ordinateur(2020), and European Project: 810367,EMC2(2019)

Subjects
computer arithmetic, Numerical Analysis, [INFO.INFO-AO]Computer Science [cs]/Computer Arithmetic, General Mathematics, Floating-point arithmetic, numerical computing
Abstract

Floating-point numbers have an intuitive meaning when it comes to physics-based numerical computations, and they have thus become the most common way of approximating real numbers in computers. The IEEE-754 Standard has played a large part in making floating-point arithmetic ubiquitous today, by specifying its semantics in a strict yet useful way as early as 1985. In particular, floating-point operations should be performed as if their results were first computed with an infinite precision and then rounded to the target format. A consequence is that floating-point arithmetic satisfies the ‘standard model’ that is often used for analysing the accuracy of floating-point algorithms. But that is only scraping the surface, and floating-point arithmetic offers much more.In this survey we recall the history of floating-point arithmetic as well as its specification mandated by the IEEE-754 Standard. We also recall what properties it entails and what every programmer should know when designing a floating-point algorithm. We provide various basic blocks that can be implemented with floating-point arithmetic. In particular, one can actually compute the rounding error caused by some floating-point operations, which paves the way to designing more accurate algorithms. More generally, properties of floating-point arithmetic make it possible to extend the accuracy of computations beyond working precision.

Published
2023

41. How to Get an Efficient yet Verified Arbitrary-Precision Integer Library

Author

Rieu-Helft, Raphaël, Marché, Claude, Melquiond, Guillaume, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Paskevich, Andrei, editor, and Wies, Thomas, editor

Published
2017
Full Text
View/download PDF

42. A Three-Tier Strategy for Reasoning About Floating-Point Numbers in SMT

Author

Conchon, Sylvain, Iguernlala, Mohamed, Ji, Kailiang, Melquiond, Guillaume, Fumex, Clément, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Majumdar, Rupak, editor, and Kunčak, Viktor, editor

Published
2017
Full Text
View/download PDF

45. Formally Verified Approximations of Definite Integrals

Author

Mahboubi, Assia, Melquiond, Guillaume, Sibut-Pinote, Thomas, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Blanchette, Jasmin Christian, editor, and Merz, Stephan, editor

Published
2016
Full Text
View/download PDF

46. Molecular Dynamics Characterization of the Conformational Landscape of Small Peptides: A Series of Hands-On Collaborative Practical Sessions for Undergraduate Students

Author

Rodrigues, João P. G. L. M., Melquiond, Adrien S. J., and Bonvin, Alexandre M. J. J.

Abstract

Molecular modelling and simulations are nowadays an integral part of research in areas ranging from physics to chemistry to structural biology, as well as pharmaceutical drug design. This popularity is due to the development of high-performance hardware and of accurate and efficient molecular mechanics algorithms by the scientific community. These improvements are also benefitting scientific education. Molecular simulations, their underlying theory, and their applications are particularly difficult to grasp for undergraduate students. Having hands-on experience with the methods contributes to a better understanding and solidification of the concepts taught during the lectures. To this end, we have created a computer practical class, which has been running for the past five years, composed of several sessions where students characterize the conformational landscape of small peptides using molecular dynamics simulations in order to gain insights on their binding to protein receptors. In this report, we detail the ingredients and recipe necessary to establish and carry out this practical, as well as some of the questions posed to the students and their expected results. Further, we cite some examples of the students' written reports, provide statistics, and share their feedbacks on the structure and execution of the sessions. These sessions were implemented alongside a theoretical molecular modelling course but have also been used successfully as a standalone tutorial during specialized workshops. The availability of the material on our web page also facilitates this integration and dissemination and lends strength to the thesis of open-source science and education.

Published
2016
Full Text
View/download PDF

47. Floating-point arithmetic

Author

Boldo, Sylvie, primary, Jeannerod, Claude-Pierre, additional, Melquiond, Guillaume, additional, and Muller, Jean-Michel, additional

Published
2023
Full Text
View/download PDF

49. Appendix: Number Theory Tools for Floating-Point Arithmetic

Author

Muller, Jean-Michel, Brisebarre, Nicolas, de Dinechin, Florent, Jeannerod, Claude-Pierre, Lefèvre, Vincent, Melquiond, Guillaume, Revol, Nathalie, Stehlé, Damien, Torres, Serge, Muller, Jean-Michel, Brisebarre, Nicolas, de Dinechin, Florent, Jeannerod, Claude-Pierre, Lefèvre, Vincent, Melquiond, Guillaume, Revol, Nathalie, Stehlé, Damien, and Torres, Serge

Published
2010
Full Text
View/download PDF

50. Extending the Precision

Author

Muller, Jean-Michel, Brisebarre, Nicolas, de Dinechin, Florent, Jeannerod, Claude-Pierre, Lefèvre, Vincent, Melquiond, Guillaume, Revol, Nathalie, Stehlé, Damien, Torres, Serge, Muller, Jean-Michel, Brisebarre, Nicolas, de Dinechin, Florent, Jeannerod, Claude-Pierre, Lefèvre, Vincent, Melquiond, Guillaume, Revol, Nathalie, Stehlé, Damien, and Torres, Serge

Published
2010
Full Text
View/download PDF

Catalog

Books, media, physical & digital resources
See catalog results