Questions tagged [lambda-calculus]

For questions about the lambda calculus, a formal mathematical model of functional computation introduced by Alonso Church

Filter by
Sorted by
Tagged with
-7 votes
3 answers
230 views

What's the point of type safety? [closed]

It has been advertised that in type-safe languages, well-typed programs never go wrong, but this doesn't like a legit statement to me: Array indexing is usually by int, but we can freely send out of ...
ice1000's user avatar
  • 2,384
1 vote
1 answer
418 views

What are some useful corollaries of the preservation theorem?

I was told that in a lambda calculus, if you have the notion of locks and concurrency, and you can prove it progress, then it means it's free of deadlocks. But is there any useful corollaries of ...
ice1000's user avatar
  • 2,384
4 votes
2 answers
171 views

What kind programming language corresponds to sequent calculus?

It is commonsense that STLC corresponds to Gentzen's natural deduction proof system, where the elimination of implication is defined in terms of modus ponens. Sequent calculus, however, is more of a &...
ice1000's user avatar
  • 2,384
3 votes
1 answer
211 views

Call-by-value: Left-to-right vs right-to-left

There are three standard evaluation strategies for the lambda calculus: Call-by-value (CBV) Call-by-name Call-by-need There are two variants of CBV that differ on how they behave with respect to ...
user76284's user avatar
  • 159
7 votes
1 answer
379 views

Possible ways for a system interface in a lazy LC language?

I'm writing a backend for lazy lambda calculus. Now I'm curious about how it could interface with the system. As an experiment, I managed to write READ and WRITE primitives, each of which does the ...
Bubbler's user avatar
  • 703
7 votes
1 answer
111 views

A lambda calculus backend without data constructors and `case`, what could go wrong?

I'm working on a lazy lambda calculus backend. I'm roughly following the concepts from Implementing functional languages: a tutorial. It presents Core as an intermediate language, and it has data ...
Bubbler's user avatar
  • 703
11 votes
1 answer
193 views

Runtime/Backend for a lazy, pure functional, lambda-calculus-based language?

I'm thinking of writing a toy language based on lambda calculus. I want it to be lazily evaluated. I/O is not a concern for now; main will be a pure function that ...
Bubbler's user avatar
  • 703