Query: coq

title: The CoQ oxidoreductase FSP1 acts in parallel to GPX4 to inhibit ferroptosis
abstract: Ferroptosis is a form of regulated cell death that is caused by the iron dependent peroxidation of lipids1,2. The glutathione dependent lipid hydroperoxidase glutathione peroxidase 4 (GPX4) prevents ferroptosis by converting lipid hydroperoxides into non toxic lipid alcohols3,4. Ferroptosis has previously been implicated in the cell death that underlies several degenerative conditions2, and induction of ferroptosis by the inhibition of GPX4 has emerged as a therapeutic strategy to trigger cancer cell death5. However, sensitivity to GPX4 inhibitors varies greatly across cancer cell lines6, which suggests that additional factors govern resistance to ferroptosis. Here, using a synthetic lethal CRISPR Cas9 screen, we identify ferroptosis suppressor protein 1 (FSP1) (previously known as apoptosis inducing factor mitochondrial 2 (AIFM2) as a potent ferroptosis resistance factor. Our data indicate that myristoylation recruits FSP1 to the plasma membrane where it functions as an oxidoreductase that reduces coenzyme Q10 (CoQ) (also known as ubiquinone 10) which acts as a lipophilic radical trapping antioxidant that halts the propagation of lipid peroxides. We further find that FSP1 expression positively correlates with ferroptosis resistance across hundreds of cancer cell lines, and that FSP1 mediates resistance to ferroptosis in lung cancer cells in culture and in mouse tumour xenografts. Thus, our data identify FSP1 as a key component of a non mitochondrial CoQ antioxidant system that acts in parallel to the canonical glutathione based GPX4 pathway. These findings define a ferroptosis suppression pathway and indicate that pharmacological inhibition of FSP1 may provide an effective strategy to sensitize cancer cells to ferroptosis inducing chemotherapeutic agents. A synthetic lethal CRISPR Cas9 screen identifies ferroptosis suppressor protein 1 as a key ferroptosis resistance factor, the expression of which correlates with ferroptosis resistance in hundreds of cancer cell lines.

title: Coq Coq correct! verification of type checking and erasure for Coq, in Coq
abstract: Coq is built around a well delimited kernel that perfoms typechecking for definitions in a variant of the Calculus of Inductive Constructions (CIC) Although the metatheory of CIC is very stable and reliable, the correctness of its implementation in Coq is less clear. Indeed, implementing an efficient type checker for CIC is a rather complex task, and many parts of the code rely on implicit invariants which can easily be broken by further evolution of the code. Therefore, on average, one critical bug has been found every year in Coq. This paper presents the first implementation of a type checker for the kernel of Coq (without the module system and template polymorphism) which is proven correct in Coq with respect to its formal specification and axiomatisation of part of its metatheory. Note that because of Godel's incompleteness theorem, there is no hope to prove completely the correctness of the specification of Coq inside Coq (in particular strong normalisation or canonicity) but it is possible to prove the correctness of the implementation assuming the correctness of the specification, thus moving from a trusted code base (TCB) to a trusted theory base (TTB) paradigm. Our work is based on the MetaCoq project which provides metaprogramming facilities to work with terms and declarations at the level of this kernel. Our type checker is based on the specification of the typing relation of the Polymorphic, Cumulative Calculus of Inductive Constructions (PCUIC) at the basis of Coq and the verification of a relatively efficient and sound type checker for it. In addition to the kernel implementation, an essential feature of Coq is the so called extraction: the production of executable code in functional languages from Coq definitions. We present a verified version of this subtle type and proof erasure step, therefore enabling the verified extraction of a safe type checker for Coq.

title: On synthetic undecidability in Coq, with an application to the Entscheidungsproblem
abstract: We formalise the computational undecidability of validity, satisfiability, and provability of first order formulas following a synthetic approach based on the computation native to Coq's constructive type theory. Concretely, we consider Tarski and Kripke semantics as well as classical and intuitionistic natural deduction systems and provide compact many one reductions from the Post correspondence problem (PCP) Moreover, developing a basic framework for synthetic computability theory in Coq, we formalise standard results concerning decidability, enumerability, and reducibility without reference to a concrete model of computation. For instance, we prove the equivalence of Post's theorem with Markov's principle and provide a convenient technique for establishing the enumerability of inductive predicates such as the considered proof systems and PCP.

title: FEther: An Extensible Definitional Interpreter for Smart Contract Verifications in Coq
abstract: Recently, blockchain technology has been widely applied in the financial field. Therefore, the security of the blockchain smart contracts is among the most popular contemporary research topics. To improve the theorem proving technology in this field, we are developing an extensible hybrid verification proof engine, denoted as FEther, for Ethereum smart contract verification. Based on Lolisa, which is a large subset of solidity mechanized in Coq, FEther guarantees the consistency between smart contracts and its formal model. Combining symbolic execution with higher order logic theorem proving, FEther contains a set of automatic strategies that execute and verify the smart contracts in Coq with a high level of automation. Besides, in FEther, the verified code segments also can be reused to assist in the verification of other properties. The functional correctness of FEther was verified in Coq. The execution efficiency of FEther has far exceeded that of the interpreters that are developed in Coq in accordance with the standard tutorial. To the best of our knowledge, FEther is the first definitional interpreter of the solidity language in Coq.

title: Hilbert's Tenth Problem in Coq
abstract: We formalise the undecidability of solvability of Diophantine equations, i.e. polynomial equations over natural numbers, in Coq's constructive type theory. To do so, we give the first full mechanisation of the Davis Putnam Robinson Matiyasevich theorem, stating that every recursively enumerable problem in our case by a Minsky machine is Diophantine. We obtain an elegant and comprehensible proof by using a synthetic approach to computability and by introducing Conway's FRACTRAN language as intermediate layer. Additionally, we prove the reverse direction and show that every Diophantine relation is recognisable by \mu$ recursive functions and give a certified compiler from \mu$ recursive functions to Minsky machines.

title: Equations reloaded: high level dependently typed functional programming and proving in Coq
abstract: Equations is a plugin for the Coq proof assistant which provides a notation for defining programs by dependent pattern matching and structural or well founded recursion. It additionally derives useful high level proof principles for demonstrating properties about them, abstracting away from the implementation details of the function and its compiled form. We present a general design and implementation that provides a robust and expressive function definition package as a definitional extension to the Coq kernel. At the core of the system is a new simplifier for dependent equalities based on an original handling of the no confusion property of constructors.

title: Interactive Theorem Proving and Program Development: Coq'Art The Calculus of Inductive Constructions
abstract: A practical introduction to the development of proofs and certified programs using Coq. An invaluable tool for researchers, students, and engineers interested in formal methods and the development of zero fault software.

title: b RA reduces DMQ/CoQ ratio and rescues the encephalopathic phenotype in Coq9 R239X mice
abstract: Coenzyme Q (CoQ) deficiency has been associated with primary defects in the CoQ biosynthetic pathway or to secondary events. In some cases, the exogenous CoQ supplementation has limited efficacy. In the Coq9R239X mouse model with fatal mitochondrial encephalopathy due to CoQ deficiency, we have tested the therapeutic potential of b resorcylic acid (b RA) a structural analog of the CoQ precursor 4 hydroxybenzoic acid and the anti inflammatory salicylic acid. b RA noticeably rescued the phenotypic, morphological, and histopathological signs of the encephalopathy, leading to a significant increase in the survival. Those effects were due to the decrease of the levels of demethoxyubiquinone 9 (DMQ9) and the increase of mitochondrial bioenergetics in peripheral tissues. However, neither CoQ biosynthesis nor mitochondrial function changed in the brain after the therapy, suggesting that some endocrine interactions may induce the reduction of the astrogliosis, spongiosis, and the secondary down regulation of astrocytes related neuroinflammatory genes. Because the therapeutic outcomes of b RA administration were superior to those after CoQ10 supplementation, its use in the clinic should be considered in CoQ deficiencies.

title: Mi Cho Coq, a framework for certifying Tezos Smart Contracts
abstract: Tezos is a blockchain launched in June 2018. It is written in OCaml and supports smart contracts. Its smart contract language is called Michelson and it has been designed with formal verification in mind. In this article, we present Mi Cho Coq, a Coq framework for verifying the functional correctness of Michelson smart contracts. As a case study, we detail the certification of a Multisig contract with the Mi Cho Coq framework.

title: A Coq Library of Undecidable Problems
abstract: We propose a talk on our library of mechanised reductions to establish undecidability results in Coq. The library is a collaborative effort, growing constantly and we are seeking more outside contributors willing to work on undecidability results in Coq.