Questions tagged [curry-howard]

The tag has no usage guidance.

35 questions
Filter by
Sorted by
Tagged with
52 views

How can we derive this representation of existential types?

I know that an existential type $\exists t. t$ can be represented using universally quantified types as $\forall r. (\forall t. t \rightarrow r) \rightarrow r$ and I have some basic intuition for ...
36 views

Axiomatic Geometry expressed with algebraic data types & functions

I've been trying to express an axiomatic geometry  using a typed functional language (OCaml so far). My motivation comes from  and the claim "Programs correspond to logical proofs". In ...
21 views

Analogue of disjunction and existence properties for a Turing-complete programming language?

Quoting from Wikipedia: In mathematical logic, the disjunction and existence properties are the "hallmarks" of constructive theories such as Heyting arithmetic and constructive set theories ...
59 views

How do program types such as natural numbers figure into the Curry-Howard Isomorphism?

In Coq, the nat, the type of natural numbers, has type Set. By the Curry-Howard Isomorphism, all propositions of type ...
58 views

What are the differences between LCF's Theorem and Automath's Prop?

How are the fundamental approaches to proving theorems by LCF and Automath different? Considering their modern descendants - Isabelle for LCF and Coq for Automath, both rely on type checking to do ...
90 views

Curry–Howard correspondence and functional programming "reliability"

The first time I heard about functional programming, someone told me "it's more reliable to code in a functional style because your type system is like a proof of correctness". I recently ...
153 views

Curry-Howard, void, and type checking in Haskell

I am trying to understand an example of theorem proving via type checking in Haskell given here. The example is as follows. Using the Curry-Howard isomorphism, construct an inhabitant of the type and ...
97 views

Understanding $\lambda \mu$-calculus in more programming way

I am learning $\lambda \mu$-calculus (self-study). I learned it because it seems very useful for understanding Curry-Howard correspondence (e.g understanding the connection between classical logic ...
609 views

Does the underlying computational calculus in type theories affect decidability?

I'm looking for a high-level explanation although if that isn't possible or difficult, I'd prefer references to books/papers. I understand that modern type theory is inspired by Curry-Howard ...
36 views

How do you derive a type $∃e(e)$ in terms of universally quantified types, without invoking Void initially?

I wrote a "proof" for this, and though it was enough to convince myself, there are a few things that bother me about it. Primarily I'm not sure about the loose way in which I'm swapping between first-...
135 views

Curry-howard isomorphism in object oriented programming languages

I want to get a better intuition for the curry howard isomorphism, and my intuition is mainly based on object oriented programming languages like JavaScript. So as an example, I am going to formalize ...
408 views

Implementing mathematical theory of arithmetic in Haskell via Curry-Howard correspondence

I have to ask for forgiveness in advance if the whole question doesn't make a lot of sense, but unfortunately, I have no better intuition as of right now and this seems like the best starting point I ...
218 views

Lambda calculus as the language of universal logic - connectives vs functions in lambda calculus?

I am reading http://okmij.org/ftp/gengo/applicative-symantics/AACG1.pdf and there is defined language TL (see last row in the table on page 4). It seems to me from this definition of TL, that lambda ...
97 views

Why algorithms calculating non-tirivial zeros can't be used as proofs of Riemann Hypothesis?

Recently I was reading again this propositions as types paper by Philip Wadler: http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf It gives an impression, ...
70 views

Is implication(function) more fundamental than lets say conjunction(product) in type theory?

According to the answer at (How to define function type in AGDA) the function type is kind of a fundamental thing in Agda and needed for bootstrapping, hence end user can not define it like what they ...
182 views

How logic programming (especially ASP) is related to the reasoning in (first-order) logic?

How logic programming (https://en.wikipedia.org/wiki/Logic_programming, especially answer set programming) is related to the reasoning in the (first-order) logic? Maybe logic programming can be ...
337 views

Can lambda-calculus be used for knowledge representation?

Natural language semantics (in computational linguistics) uses lambda terms for expressing the semantics of natural language sentences. There is vast literature about combinatorial categorial grammars ...
519 views

Curry Howard correspondence to Predicate Logic?

So I'm trying to get my head round Curry-Howard. (I've tried at it several times, it's just not gelling/seems too abstract). To tackle something concrete, I'm working through the couple of Haskell ...
70 views

What is the role of abstract machines in the Curry-Howard isomorphism?

By abstract machines I mean things like the SECD machine, Krivine's machine or more generally machines with states/memory/registers/stack/accumulator... According to Wikipedia page of the Curry-...
145 views

Can a type system serve as a proof assistant for foreign functions?

Given that: A language with very expressive type systems (e.g. Idris) can also have escape mechanisms like foreign function interfaces/unsafePerformIO. There are proof assistants that can be used to ...
807 views

forall a b, a -> b [duplicate]

I know for pretty sure that there is a function with the type $f: \forall \alpha, \beta . \alpha \rightarrow \beta$ (at least in a Hindley-Milner type system), but I can't wrap my head over it. ...
213 views

Why Church-encoded types aren't sufficient to express inductive proofs?

I've heard some claims that the calculus of constructions without inductive types isn't powerful enough to express proofs by induction. Is that correct? If so, why isn't the Church-encoding sufficient ...
754 views

Is there an isomorphism between (subset of) category theory and relational algebra?

It comes from big data perspective. Basically, many frameworks (like Apache Spark) "compensate" lack of relational operations by providing Functor/Monad-like interfaces and there is a similar movement ...
52 views

Curry howard Isomorphism what the propositions A , B ranges over

In CH-I what the propositions A , B ranges over too ? An update : From Pfennings notes : "A denotes proposition about the mathematical objects such as integer or a real number." From : Per ...
162 views

Curry howard isomorphism "proof as program"

I'm reading CH Isomorphism. Let's divide into two stages: Prop corresponds to types. so a proposition A $\wedge$ B corresponds to type A $\times$ B. Proof corresponds to the program. What is the ...
99 views