Coq Change Analytics: A Superhero Origin Story & Research Recruitment Video

One Seattle summer day, a proof engineer is struggling to get his Coq proofs to go through. Together with heroes The Eliminator and The Tactician, he devises a plan to help not just himself, but the Coq community more broadly. In doing so, he, too, becomes a hero.

His plan is to help contribute his data to the Coq Change Analytics study. You can join him, and become a hero too. (We'll give you a superhero name if you want one.) If you are interested, please fill out this screening survey: We will be in touch if you are eligible. The full study description is below.

---

Study Description

In recent years, verification efforts using proof assistants like like Coq have reached large, critical software projects. In spite of this, there is little data on the development processes of proof engineers. We are deploying a Coq plugin to a group of proof engineers that collects data on the changes that proof engineers make in development, then analyzing the data and using it to inform the next generation of proof automation tooling.

Getting Involved: If you are interested in participating, please fill out this screening survey at We will be in touch if you are eligible. Filling out this survey is not a commitment to participate.

The only requirements to get involved are that you are 18 years or older, fluent in English, and have at least a year of experience using the Coq proof assistant.

Study Details: During the study, we will send you a link to install our Coq plugin. To install this plugin, you will need a recent version of Coq. You may use any editor or development environment. The plugin will ask you a few questions about your background and development environment the first time you install it.

After that, we will ask you to continue normal Coq development with the plugin installed for a period of one month, running from August 7th through September 7th. The plugin will collect data on the changes that you make in development, which we will later analyze.

Data Details: If you choose to participate, we will collect your name and email address for screening purposes and for later contact; this information will not be linked to the study data or to any publications.

The plugin will collect the changes that you make to Coq developments, including changes to definitions and proofs, as well as how you step through the file interactively. The plugin will assign you a unique identifier and store this data linked to that unique identifier in a server.

We will analyze the resulting data and use the results of our analysis to write a research paper on the development practices of proof engineers in Coq. We will also use the results of our analysis to inform the design of a proof patching tool and of a machine learning tool for tactics. We will also release the data for use in other research.

If you choose to participate, we will send you a consent form with more details.

Benefits: We anticipate that our work will benefit the broader community of proof engineers, and we plan to make the dataset publicly available. We will also use the data to write a paper on the processes of proof engineers, as well as to inform the development of tools for automated proof repair and machine learning for proof automation so that these tools meet the needs of real proof engineers like you.

---

Cast & Crew

Narrator: Dimitar Bounov, UCSD Alumnus

Proof engineer/Mr. QED: Martin Kellogg, UW

Friend: Chandrakana Nandi, UW

The Eliminator: Talia Ringer, UW

The Tactician: Alex Sanchez-Stern, UCSD

Director: Talia Ringer, UW

Filming: Doug Woos, UW Alumnus

Video Editing: Alex Sanchez-Stern, UCSD

Pun Consultants: Karl Palmskog, UT Austin & Dan Grossman, UW

Read More

Tips to Publish Your Research Paper.

Publishing Paper is time taking many times. But it is worth if you do it rightly. Here are tips on how to publish your research paper and at the same time adding quality. Here is my excellent article on how to do it.

Read More

How to publish a research paper in Springer Journals

The FAQs of a Journal are already listed in a previous video. a Springer Journal is taken and explained how to see FAQ for the possible publication in the journal

Read More

How to Write an Original Research Paper That Will Get Published │ Dr. Willias Masocha

Introduction:

Good research findings have to be published in order to be read widely, be easily accessible to both the public and other scientists and further science. Most scientists have heard of or come across the phrase “publish or perish”. This is because in addition to scientific communication publishing is also essential for the survival of the scientists and the scientific work they do. Publications are used as indices of ability and/or success in order to get or maintain funding for research, getting a position or career advancement, attract graduate students etc. The components of an original research manuscript that are essential for it to be successfully published in a good scientific journal are the scientific idea, research methodology, results obtained and presentation i.e. how the manuscript is written. Poor writing leads to manuscript rejection or delay in publication despite good science. Good writing is essential for the editor, reviewer and the reader to understand what research was done and what it means or contributes. Unfortunately, most scientists complete their education without a structured training in scientific writing. A major goal of this webinar is filling part of this gap, in order to enhance successful publication of manuscripts.

In this webinar you will learn about:

What is an original research paper?

General structure of an original research paper and how to write each section of the paper

Steps to organizing a research paper

Three important things to consider when writing a manuscript: language and grammar, content and presentation

Importance about selecting the right journal

Questions to ask oneself before and after writing a manuscript

Speaker:

Willias Masocha, PhD

Associate Professor

Department of Pharmacology and Therapeutics

Faculty of Pharmacy, Kuwait University

Biosketch:

Willias Masocha is an Associate Professor in the Department of Pharmacology and Therapeutics, Faculty of Pharmacy, Kuwait University, Kuwait. He received his Bachelor of Pharmacy Honours from the University of Zimbabwe in 1997 and Ph.D. degree in Pharmacology from the University of Granada, Spain, in 2002. He was a Postdoctoral Fellow & International Brain Research Organization Research (IBRO) Fellow in Prof. Krister Kristensson’s lab at the Department of Neuroscience, Karolinska Institute, Sweden, from 2003 to 2006 working on the role of the immune system on the entrance of parasites into the CNS and the neuropathogenesis of African trypanosomiasis. His research program at Kuwait University focuses on studying the pathophysiology of various types of pain, especially chemotherapy and antiretroviral drug-induced neuropathic pain, and evaluation of the activities of potential anti-inflammatory and/or analgesic drugs. He is also interested in neuroinflammation mainly the study of astrocytes and microglia activation during neuropathic pain as well as that induced by endotoxins or infections.

He has an intense interest in scientific writing and believes it should be taught in all science related graduate programs and to all scientists. In 2014 he completed a Stanford University online course “Writing in the Sciences”. In 2017 he participated in the IBRO-ARC Writing Papers Workshop in Entebbe, Uganda (organized by Prof. Marina Bentivoglio) as an instructor and mentor giving lectures on how to write scientific papers and mentoring students on how to write and edit their own manuscripts. In March 2019 in Lagos, Nigeria he will be participating as an instructor and mentor in another IBRO-ARC Writing Papers Workshop. He also incorporates scientific writing and presentation elements in other IBRO schools that he participates in as well as the MSc course, Central Neuropharmacology, which he coordinates and teaches at Kuwait University

Willias Masocha,

Mosab Ali Awadelkareem, Al-Neelain University, Sudan.

Maha Dahawi, University of Khartoum, Sudan.

Cynthia Lefebvre Omar, Sorbonne University, France.

Inas Ahmed Elsayed, University of Gezira, Sudan.

TReND in Researchers

Read More