Concept

Calcul infinitésimal

Publications associées (39)

SC-TPTP: An Extension of the TPTP Derivation Format for Sequent-Based Calculus

Motivated by the transfer of proofs between proof systems, and in particular from first order automated theorem provers (ATPs) to interactive theorem provers (ITPs), we specify an extension of the TPTP derivation text format to describe proofs in first-ord ...

2024

A Mechanized Theory of the Box Calculus

Yichen Xu

Capture calculus is an extension of System Fsub that tracks free variables of terms in their type, allowing one to represent capabilities while limiting their scope. While previous calculi had mechanized soundness proofs, the latest version, namely the box ...

2023

Revisiting the General Identifiability Problem

Negar Kiyavash, Ehsan Mokhtarian, Yaroslav Kivva, Seyed Jalal Etesami

We revisit the problem of general identifiability originally introduced in [Lee et al., 2019] for causal inference and note that it is necessary to add positivity assumption of observational distribution to the original definition of the problem. We show t ...

2022

Type-Level Programming with Match Types

Martin Odersky, Olivier Eric Paul Blanvillain

Type-level programming is becoming more and more popular in the realm of functional programming. However, the combination of type-level programming and subtyping remains largely unexplored in practical programming languages. This paper presents match types ...

ASSOC COMPUTING MACHINERY2022

A Continuized View on Nesterov Acceleration

Nicolas Henri Bernard Flammarion, Raphaël Jean Berthier

We introduce the "continuized" Nesterov acceleration, a close variant of Nesterov acceleration whose variables are indexed by a continuous time parameter. The two variables continuously mix following a linear ordinary differential equation and take gradien ...

2021

On the stress tensor light-ray operator algebra

Grégoire Olivier Mathys, Matthew Thomas Walters, Alexandre Mathieu Frédéric Belin

We study correlation functions involving generalized ANEC operators of the form integral dx-x-n+2T--x -> in four dimensions. We compute two, three, and ...

2021

A Mechanized Theory of Quoted Code Patterns

The pattern matching on code from the new macro system of Scala 3 is modeled by a calculus called λ half-circle. We present a mechanized proof of soundness of the calculus in Coq and discuss encountered challenges. ...

2020

Integral Convexity And Parabolic Systems

Bernard Dacorogna

In this work we give optimal, i.e., necessary and sufficient, conditions for integrals of the calculus of variations to guarantee the existence of solutions-both weak and variational solutions-to the associated L-2-gradient flow. The initial values are mer ...

SIAM PUBLICATIONS2020

Formal foundations for GADTs in Scala

GADTs are a very useful language feature that allow encoding some invariants in types. GADT reasoning is currently implemented in Scala and Dotty, but it’s plagued with soundness issues. To get a better understanding of GADTs in Scala, we explore how they ...

2020

The Essence of Dependent Object Types

Martin Odersky, Tiark Rompf, Nada Amin, Sandro Stucki, Karl Samuel Grütter

Focusing on path-dependent types, the paper develops foundations for Scala from first principles. Starting from a simple calculus D-

Springer International Publishing2016

Graph Chatbot

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.

Connectez-vous pour utiliser Chat avec Graph Search