Publications related to Corecursion

Acceleration of graph pattern mining and applications to financial crime

Various forms of real-world data, such as social, financial, and biological networks, can be represented using graphs. An efficient method of analysing this type of data is to extract subgraph patterns, such as cliques, cycles, and motifs, from graphs. For ...

EPFL2023

Recursive evaluation and iterative contraction of N-body equivariant features

Michele Ceriotti, Sergey Pozdnyakov, Jigyasa Nigam

Mapping an atomistic configuration to a symmetrized N-point correlation of a field associated with the atomic positions (e.g., an atomic density) has emerged as an elegant and effective solution to represent structures as the input of machine-learning algo ...

2020

Verified Functional Programming

Nicolas Charles Yves Voirol

In this thesis, we present Stainless, a verification system for an expressive subset of the Scala language. Our system is based on a dependently-typed language and an algorithmic type checking procedure which ensures total correctness. We rely on SMT solve ...

EPFL2019

Contract-Based Resource Verification for Higher-Order Functions with Memoization

Viktor Kuncak, Ravichandhran Kandhadai Madhavan, Sumith Kulal

We present a new approach for specifying and verifying resource utilization of higher-order functional programs that use lazy evaluation and memoization. In our approach, users can specify the desired resource bound as templates with numerical holes e.g. a ...

Assoc Computing Machinery2017

Algorithmic Resource Verification

Ravichandhran Kandhadai Madhavan

Static estimation of resource utilisation of programs is a challenging and important problem with numerous applications. In this thesis, I present new algorithms that enable users to specify and verify their desired bounds on resource usage of functional p ...

EPFL2017

Optimization Of Compound Regularization Parameters Based On Stein'S Unbiased Risk Estimate

Xin Liu, Hanjie Pan, Feng Xue, Jiaqi Liu

Recently, the type of compound regularizers has become a popular choice for signal reconstruction. The estimation quality is generally sensitive to the values of multiple regularization parameters. In this work, based on BDF algorithm, we develop a data-dr ...

Ieee2017

Explicit Recursive and Adaptive Filtering in Reproducing Kernel Hilbert Spaces

Devis Tuia

This brief presents a methodology to develop recursive filters in reproducing kernel Hilbert spaces. Unlike previous approaches that exploit the kernel trick on filtered and then mapped samples, we explicitly define the model recursivity in the Hilbert spa ...

Ieee-Inst Electrical Electronics Engineers Inc2014

turboTDDFT 2.0 Hybrid functionals and new algorithms within time-dependent density-functional perturbation theory

We present a new release of the turboTDDFT code featuring an implementation of hybrid functionals, a recently introduced pseudo-Hermitian variant of the Liouville-Lanczos approach to time-dependent density-functional perturbation theory, and a newly develo ...

Elsevier Science Bv2014

An overview of the Leon verification system: verification by translation to recursive functions

Viktor Kuncak, Etienne Kneuss, Philippe Paul Henri Suter, Régis William Blanc

We present the Leon verification system for a subset of the Scala programming language. Along with several functional features of Scala, Leon supports imperative constructs such as mutations and loops, using a translation into recursive functional form. Bo ...

2013

Infinite integrals with the weighted averages algorithm

Juan Ramon Mosig, Athanasios Polymeridis

A new version of the weighted averages (WA) algorithm, called generalized WA, is introduced. Generalized WA exhibit a more compact formulation, devoid of iterative and recursive steps, and a wider range of applications. It is more robust, as it provides a ...

2011

Decision Procedures for Algebraic Data Types with Abstractions

Viktor Kuncak, Philippe Paul Henri Suter, Mirco Dotta

We describe a family of decision procedures that extend the decision procedure for quantifier-free constraints on recursive algebraic data types (term algebras) to support recursive abstraction functions. Our abstraction functions are catamorphisms (term a ...

2010

Runtime Checking for Separation Logic

Viktor Kuncak

Separation logic is a popular approach for specifying properties of recursive mutable data structures. Several existing systems verify a subclass of separation logic specifications using static analysis techniques. Checking data structure specifications du ...

Springer2008