In type theory with an impredicative universe of propositions and a
proof-irrelevant propositional equality the normalization property fails. Thus,
type checking is likely undecidable. The counterexample to normalization is
adapted from Girard's counterexample against normalization of System F equipped
with a decider for type equality. It refutes Werner's normalization conjecture
[LMCS 2008].

more |
pdf
| html
None.

ranha:
Abel & Coquandのこれ読んでたけど、この辺のloop termやら⊥-termの出てくる出てこないみたいなのの分類図欲しいな proof-irrelevant propeqとGeuversが使った {A}+{¬A}の関係性ってどうなってるんだろう
https://t.co/ofC6ELuHY1

arxiv_cslo:
Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality https://t.co/2btc3hhDQl

t6s:
RT @arxiv_cslo: Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality https://t.co/2btc3hhDQl

None.

None.

Sample Sizes : None.

Authors: 2

Total Words: 0

Unqiue Words: 0

LTLf synthesis is the automated construction of a reactive system from a
high-level description, expressed in LTLf, of its finite-horizon behavior. So
far, the conversion of LTLf formulas to deterministic finite-state automata
(DFAs) has been identified as the primary bottleneck to the scalabity of
synthesis. Recent investigations have also shown that the size of the DFA state
space plays a critical role in synthesis as well.
Therefore, effective resolution of the bottleneck for synthesis requires the
conversion to be time and memory performant, and prevent state-space explosion.
Current conversion approaches, however, which are based either on
explicit-state representation or symbolic-state representation, fail to address
these necessities adequately at scale: Explicit-state approaches generate
minimal DFA but are slow due to expensive DFA minimization. Symbolic-state
representations can be succinct, but due to the lack of DFA minimization they
generate such large state spaces that even their symbolic representations
cannot...

more |
pdf
| html
None.

arxiv_cslo:
Hybrid Compositional Reasoning for Reactive Synthesis from Finite-Horizon Specifications https://t.co/vL64Dx1Z6l

None.

None.

Sample Sizes : None.

Authors: 4

Total Words: 0

Unqiue Words: 0

The paper is focused on temporal logics for the description of the behaviour
of real-time pushdown reactive systems. The paper is motivated to bridge
tractable logics specialized for expressing separately dense-time real-time
properties and context-free properties by ensuring decidability and
tractability in the combined setting. To this end we introduce two real-time
linear temporal logics for specifying quantitative timing context-free
requirements in a pointwise semantics setting: Event-Clock Nested Temporal
Logic (EC_NTL) and Nested Metric Temporal Logic (NMTL). The logic EC_NTL is an
extension of both the logic CaRet (a context-free extension of standard LTL)
and Event-Clock Temporal Logic (a tractable real-time logical framework related
to the class of Event-Clock automata). We prove that satisfiability of EC_NTL
and visibly model-checking of Visibly Pushdown Timed Automata (VPTA) against
EC_NTL are decidable and EXPTIME-complete. The other proposed logic NMTL is a
context-free extension of standard Metric Temporal Logic...

more |
pdf
| html
None.

arxiv_cslo:
Timed Context-Free Temporal Logics https://t.co/m11lU8gb4S

None.

None.

Sample Sizes : None.

Authors: 3

Total Words: 0

Unqiue Words: 0

This paper introduces an expressive class of quotient-inductive types, called
QW-types. We show that in dependent type theory with uniqueness of identity
proofs, even the infinitary case of QW-types can be encoded using the
combination of inductive-inductive definitions, Hofmann-style quotient types,
and Abel's size types. The latter, which provide a convenient constructive
abstraction of what classically would be accomplished with transfinite
ordinals, are used to prove termination of the recursive definitions of the
elimination and computation properties of our encoding of QW-types. The
development is formalized using the Agda theorem-prover.

more |
pdf
| html
None.

arxiv_cslo:
Constructing Infinitary Quotient-Inductive Types https://t.co/9vho9eE7c2

t6s:
RT @arxiv_cslo: Constructing Infinitary Quotient-Inductive Types https://t.co/9vho9eE7c2

None.

None.

Sample Sizes : None.

Authors: 3

Total Words: 8885

Unqiue Words: 2252

Classes with bounded rankwidth are MSO-transductions of trees and classes
with bounded linear rankwidth are MSO-transductions of paths. These results
show a strong link between the properties of these graph classes considered
from the point of view of structural graph theory and from the point of view of
finite model theory. We take both views on classes with bounded linear
rankwidth and prove structural and model theoretic properties of these classes:
1) Graphs with linear rankwidth at most $r$ are linearly \mbox{$\chi$-bounded}.
Actually, they have bounded $c$-chromatic number, meaning that they can be
colored with $f(r)$ colors, each color inducing a cograph. 2) Based on a
Ramsey-like argument, we prove for every proper hereditary family $\mathcal F$
of graphs (like cographs) that there is a class with bounded rankwidth that
does not have the property that graphs in it can be colored by a bounded number
of colors, each inducing a subgraph in~$\mathcal F$. 3) For a class $\mathcal
C$ with bounded linear rankwidth the following...

more |
pdf
| html
None.

None.

None.

Sample Sizes : None.

Authors: 4

Total Words: 17050

Unqiue Words: 2827

In ESOP 2008, Gulwani and Musuvathi introduced a notion of cover and
exploited it to handle infinite-state model checking problems. Motivated by
applications to the verification of data-aware processes, we proved in a
previous paper that covers are strictly related to model completions, a
well-known topic in model theory. In this paper we investigate cover transfer
to theory combinations in the disjoint signatures case. We prove that for
convex theories, cover algorithms can be transferred to theory combinations
under the same hypothesis (equality interpolation property aka strong
amalgamation property) needed to transfer quantifier-free interpolation. In the
non-convex case, we show by a counterexample that cover may not exist in the
combined theories. However, we exhibit a cover transfer algorithm operating
also in the non-convex case for special kinds of theory combinations; these
combinations (called `tame combinations') concern multi-sorted theories arising
in many model-checking applications (in particular, in...

more |
pdf
| html
None.

None.

None.

Sample Sizes : None.

Authors: 5

Total Words: 9950

Unqiue Words: 1973

Assert is a website where the best academic papers on arXiv (computer science, math, physics), bioRxiv (biology), BITSS (reproducibility), EarthArXiv (earth science), engrXiv (engineering), LawArXiv (law), PsyArXiv (psychology), SocArXiv (social science), and SportRxiv (sport research) bubble to the top each day.

Papers are scored (in real-time) based on how verifiable they are (as determined by their Github repos) and how interesting they are (based on Twitter).

To see top papers, follow us on twitter @assertpub_ (arXiv), @assert_pub (bioRxiv), and @assertpub_dev (everything else).

To see beautiful figures extracted from papers, follow us on Instagram.

*Tracking 225,737 papers.*

Sort results based on if they are interesting or reproducible.

Interesting

Reproducible