2

I am not sure I understand your question, but I believe the answer is "yes". When describing monomorphic languages, an expression such as let id x = x : τ (where τ is understood as a type meta-variable) does not mean that you can write τ in the program text. Rather, it means an arbitrary expression of that shape, where the meta-variable is replaced by ...


1

The relationship between the two is related to intuistionistic logic vs. classical logic. When you add sufficiently powerful versions of the excluded middle law to Curry-Howard-style type systems, you can translate between propositions (types of sort Prop, which are inhabited if and only if they are provable) and Boolean values at will. Check out the list of ...


1

Does it mean that a logic system is a programming language, where types are propositions and values of a type are proofs of the proposition? Not necessarily, being both (logic systems and programming language) formal languages, there certainly is a certain degree of isomorphism between the two concepts, this translates into the fact that we can encode a ...


1

The terminology used in the database area calls the relational algebra “procedural” to contrast it with the languages based on “calculus”, since an algebraic expression describes an ordered set of steps to find the result: simply execute the operations in the correct order to produce the result. In contrast, in an expression of a calculus based language, ...


Only top voted, non community-wiki answers of a minimum length are eligible