English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Higher-order logic HOL offers a very simple syntax and semantics forrepresenting and reasoning about typed data structures. But its type systemlacks advanced features where types may depend on terms. Dependent type theoryoffers such a rich type system, but has rather substantial conceptualdifferences to HOL, as well as comparatively poor proof automation support. Weintroduce a dependently-typed extension DHOL of HOL that retains the style andconceptual framework of HOL. Moreover, we build a translation from DHOL to HOLand implement it as a preprocessor to a HOL theorem prover, thereby obtaining atheorem prover for DHOL.

Theorem Proving in Dependently-Typed Higher-Order Logic -- Extended Preprint