Efficient Parsing with Derivatives and Zippers

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.

As a universal expression of human creativity, music is capable of conveying great subtlety and complexity. Crucially, this complexity is not encoded in the score or in the sounds, but is rather construed in the mind of the listener in the form of nuanced ...

We study the proof theory and algorithms for orthologic, a logical system based on ortholattices, which have shown practical relevance in simplification and normalization of verification conditions. Ortholattices weaken Boolean algebras while having polyno ...

In this paper, we present a model for the analytical computation of the power flow sensitivity coefficients (SCs) for hybrid AC/DC networks. The SCs are defined as the partial derivates of the nodal voltages with respect to the active and reactive power in ...

Recently, the diffusion moving-average (D-MA) scheme has been proposed as a way to combat noisy links over adaptive networks. However, the current theoretical results focus on networks with mean-square error costs where the optimal local solution agrees wi ...

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 ...

Formally verifying the correctness of software is necessary to merit the trust people put in software systems. Currently, formal verification requires human effort to prove that a piece of code matches its specification and code changes to improve verifiab ...

While theoretical and empirical insights suggest that the capacity to represent and process complex syntax is crucial in language as well as other domains, it is still unclear whether specific parsing mechanisms are also shared across domains. Focusing on ...

Formal verification of real-world software systems remains challenging for a number of reasons, including lack of automation, friction in specifying properties, and limited support for the diverse programming paradigms used in industry. In this thesis we m ...

Advances in mobile computing have paved the way for new types of distributed applications that can be executed solely by mobile devices on Device-to-Device (D2D) ecosystems (e.g., crowdsensing). Sophisticated applications, like cryptocurrencies, need distr ...

As it has become easier and cheaper to collect big datasets in the last few decades, designing efficient and low-cost algorithms for these datasets has attracted unprecedented attention. However, in most applications, even storing datasets as acquired has ...

Interactive oracle proofs (IOPs) are a proof system model that combines features of interactive proofs (IPs) and probabilistically checkable proofs (PCPs). IOPs have prominent applications in complexity theory and cryptography, most notably to constructing ...

We propose a new approach for normalization and simplification of logical formulas. Our approach is based on algorithms for lattice-like structures. Specifically, we present two efficient algorithms for computing a normal form and deciding the word problem ...

Music can be interpreted by attributing syntactic relationships to sequential musical events, and, computationally, such musical interpretation represents an analogous combinatorial task to syntactic processing in language. While this perspective has been ...

Pearl's do calculus is a complete axiomatic approach to learn the identifiable causal effects from observational data. When such an effect is not identifiable, it is necessary to perform a collection of often costly interventions in the system to learn the ...

Fuzzers aware of the input grammar can explore deeper program states using grammar-aware mutations. Existing grammar-aware fuzzers are ineffective at synthesizing complex bug triggers due to: (i) grammars introducing a sampling bias during input generation ...

We present LISA, a proof system and proof assistant for constructing proofs in schematic first-order logic and axiomatic set theory. The logical kernel of the system is a proof checker for first-order logic with equality and schematic predicate and fun ...

It is well known that hyperedge-replacement grammars can generate NP-complete graph languages even under seemingly harsh restrictions. This means that the parsing problem is difficult even in the non-uniform setting, in which the grammar is considered to b ...

This paper presents a theoretical analysis of linear interpolation as a principled method for stabilizing (large-scale) neural network training. We argue that instabilities in the optimization process are often caused by the nonmonotonicity of the loss lan ...

This paper reports on the computation of a discrete logarithm in the finite field F-230750, breaking by a large margin the previous record, which was set in January 2014 by a computation in F-29234. The present computation made essential use of the elimina ...

Modern machine learning (ML) models are capable of impressive performances. However, their prowess is not due only to the improvements in their architecture and training algorithms but also to a drastic increase in computational power used to train them.|S ...

Efficient Parsing with Derivatives and Zippers

Chat with Graph Search

Hearing structure in music: An empirical inquiry into listening as representation and processing

Orthologic with Axioms

Analytical Computation of the Sensitivity Coefficients in Hybrid AC/DC Networks

Diffusion Moving-Average Adaptation Over Networks

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

Automated Formal Verification of Software Network Functions

Musical Garden Paths: Evidence for Syntactic Revision Beyond the Linguistic Domain

Scaling Language Features for Program Verification

Toward Mobile Distributed Ledgers

Sketches, metrics and fast algorithms

A Toolbox for Barriers on Interactive Oracle Proofs

Formula Normalizations in Verification

Interpreting Rhythm as Parsing: Syntactic-Processing Operations Predict the Migration of Visual Flashes as Perceived During Listening to Musical Rhythms

Minimum Cost Intervention Design for Causal Effect Identification

Gramatron: Effective Grammar-Aware Fuzzing

LISA – A Modern Proof System

Uniform parsing for hyperedge replacement grammars

Stable Nonconvex-Nonconcave Training via Linear Interpolation

Computation Of A 30750-Bit Binary Field Discrete Logarithm

Byzantine-Resilient Learning Beyond Gradients: Distributing Evolutionary Search