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

Two major applications of lambda calculi in computer science are functional programming languages and mechanized reasoning systems (or, proof assistants). According to the Curry–Howard correspondence, it is possible, in principle, to design a unified language based on a typed lambda calculus for both logical reasoning and programming. However, the different requirements of programming languages and reasoning systems make it difficult to design such a unified language useful for both purposes. Programming languages usually extend lambda calculi with programming-friendly features (e.g., recursive datatypes, general recursion) for supporting the flexibility to model various computations, while sacrificing logical consistency. Logical reasoning systems usually extend lambda calculi with logic-friendly features (e.g., induction principles, dependent types) for paradoxfree inference over fine-grained properties, while being more restrictive in modeling computations. In this dissertation, we design and implement a language called Nax that balances between the benefits of both. Nax accepts all recursive datatypes, thus, allowing the same flexibility of defining recursive datatypes as functional languages. Nax supports a number of Mendler-style recursion schemes that can express various kinds of recursive computations and also grantee termination. Nax supports termindexed types to support specifications of fine-grained properties. In addition, Nax supports a conservative extension of Hindley–Milner type inference. The theoretical contributions of this dissertation include theories for Mendlerstyle recursion schemes and term-indexed types, which we developed to establish strong normalization and logical consistency of Nax.

The Nax Language: Unifying Functional Programming and Logical Reasoning in a Language based on Mendler-style Recursion Schemes and Term-indexed Types