User loginNavigation 
LtU ForumLambda calculusI have written a small introduction to untyped lambda calculus. The article contains nothing new, but it has been written to be easy to understand. The article is not only elementary. It contains all essential results of untyped lambda calculus like the Church Rosser theorem and some undecidability theorems. I have tried to use graphic notations to make the content more digestible and closer to intuition. I am especially proud of the proof of the Church Rosser theorem which (hopefully) is more understandable in this article than in many other presentations I have read so far. Higher Order Functions Considered Unnecessary for Higher Order ProgrammingJoseph A. Goguen, Higher Order Functions Considered Unnecessary for Higher Order Programming (1987).
This (old paper) proposes an interesting approach for formulating functional programs. But can this truly subsume all uses of higher order functions? I don't see the paper address how the uses of higher order functions in general can be replaced (not that I have a counterexample in mind). Anyone familiar with the OBJ language? Do other languages share this notion of 'modules', 'theories'? Prior art for reifying lifecycleAre there any prior examples of programming languages that expose the program processing lifecycle as a value or syntax element? By lifecycle, I mean steps like the below which many languages follow (though not necessarily in order):
Does anyone have pointers to designs of languages that allow parts of the program to run at many of these stages *and* explicitly represent the lifecycle stage as a value or syntax element? I'm aware of reified time in hardware description languages like Verilog and in event loop concurrent languages like JavaScript and E, but that's not what I'm after. Background I work in computer security engineering and run into arguments like "we can either ship code with dynamic languages that is hard to reason about the security properties of, or not ship in time." I'm experimenting with ways to enable features like the below but without the exposure to security vulnerabilities or difficulty in bringing sound static analysis to bear that often follows:
I was hoping that by allowing a high level of dynamism before untrusted inputs reach the system I could satisfy most of the use cases that motivate "greater dynamism > greater developer productivity" while still producing static systems that are less prone to unintended changes in behavior when exposed to crafted inputs. I was also hoping, by not having a single macrosrunnow stage before runtime, to allow use cases that are difficult with hygienic macros while still allowing a module to limit how many assumptions about the language another module might break by reasoning about how early in the lifecycle it imports external modules. The end goal would be to inform language design committees that maintain widely used languages. cheers, Upward confluence in the interaction calculusThe lambda calculus is not upward confluent, counterexamples being known for a long time. Now, what about the interaction calculus? Specifically, I am looking for configurations c_{1} and c_{2} that have the same normal form with no such c that c →* c_{1} and c →* c_{2}. Update: a necessary and sufficient condition for strong upward confluence discussed in arXiv:1806.07275v3 which also shows that the condition is not necessary for upward confluence by showing upward confluence for the interaction system of the linear lambda calculus. New DSL for secueityHello,thought I’d share a new DSL by endgame life querying security logs : https://www.endgame.com/blog/technicalblog/introducingeventquerylanguage It is meant to help reason about security events. Best illustrated in this example: What files were created by nonsystem users, first ran as a nonsystem process, and later ran as a systemlevel process within an hour? I think that there is a lot of improvement that can be had in. languages that help reason about (time) series and it’s a welcome addition to the DSL family. By True Konrads at 20180605 23:31  LtU Forum  login or register to post comments  other blogs  1113 reads
I have a problem with arguments passed as nonevaluated expressionsSo, since I've learned about Kernel I was very excited: the idea of explicit evaluation seemed like a very cool idea, giving much more power to the programmer in comparison to the standard "pass evaluated arguments" strategy (1: this statement can be argued upon; 2: there were numerous posts here at LtU and other blogs about potential drawbacks). So far as I've seen the problem is solved on an interpreter level, where this kind of thing is handled "behind the scenes". Sorry if this is a mess, I hope someone undestands it :) C++ fun
Proof system for learning basic algebraI've written a system for learning basic algebra which has you solve problems by clicking on the rules of basic algebra (commutativity, associativity, etc.). It is impossible to make mistakes because the machine checks things like correct handling of division by zero. Each step is justified, so each solution serves as a formal proof. Right now it handles algebra up to quadratic equations and simultaneous equations. It is intended to be a computer proof system anyone can learn. The style of mathematics presented mimics equation solving on a blackboard, so it should be familiar to everyone. Type BombsPeople like blowing stuff up, explosions are great! I started wondering about type bombs, small expressions which have large type terms. Is there anything known about that, in particular for Haskell/ML since these are popular? The small bomb I know of employs 'dup' and is relatively well known. I.e., take `dup`
The repeated application gives back a type term which grows exponentially in the size of the expression.
(It depends on the type checker, of course, whether the type actually is represented exponentially.) You can lift `dup` further but can you grow faster? I tried `let t = (\f > f . f) in let d = (\x > (x,x)) in (t.t.t.t) d 0` which doesn't type check in ghci as a first order approximation. But I thought I would ask you, people. What is the fastest growing type term you can come up with? Or what term will keep a type checker really, really busy? The Heron Programming LanguageI wanted to share some progress on a new functional statically typed language, called Heron, that I have been working on. There is a demo of some 3D at https://cdiggins.github.io/heronlanguage/. Some of you might remember earlier projects that I posted many years ago also called Heron, but this language is quite a departure from earlier work. This new language is designed for numerical and array processing (e.g. 3D and 2D graphics). I'm very interested in any and all feedback. I'm also looking for opportunities for collaborations. Thanks in advance! By cdiggins at 20180427 04:46  LtU Forum  login or register to post comments  other blogs  1621 reads

Browse archivesActive forum topics 
Recent comments
30 min 14 sec ago
1 hour 59 min ago
3 hours 46 min ago
5 hours 6 min ago
10 hours 59 min ago
1 day 2 hours ago
1 day 2 hours ago
1 day 3 hours ago
1 day 3 hours ago
1 day 4 hours ago