gasche
  • Member for 10 years, 8 months
  • Last seen this week
Why isn't it possible to recover/resume after an Exception?
Accepted answer
18 votes

"Resumable exceptions" are indeed a well-known idea in some programming language circles. In particular, Common Lisp has had resumable exceptions for a long time (so they are really not confined to ...

View answer
Has the semantics of TeX (as a programming language) ever been formalized?
11 votes

No, to my knowledge there has been no work on formalizing TeX of the kind you are interested in. (What follows is a subjective and personal commentary). I think it is an intriguing and well-posed ...

View answer
Are there any annotated formal verification systems for pure functional programming languages?
11 votes

See also Yann Régis-Gianas PhD thesis work with François Pottier: A Hoare Logic for Call-by-Value Functional Programs (MPC'08). This work was extended to cover the usual ML side-effects by Johannes ...

View answer
What's the definition of join on iso-recursive types?
8 votes

I thought a bit about this and I am afraid that it is harder than it looks -- as you suspected! In the spirit of encouraging discussion, I'll write my chain of thoughts. The subtyping rules are often ...

View answer
Formal semantics of OCaml in Coq
8 votes

You could be interested in Jacques Garrigue's A Certified Implementation of ML with Structural Polymorphism and Recursive Types, which establishes the soundness of static and dynamic semantics and ...

View answer
Can one automate algorithmic analysis?
Accepted answer
8 votes

Implicit Complexity has taught us that (some) complexity classes can be classified by type systems, in the sense that there are type systems that only accept polynomial programs, for example. One more ...

View answer
What's new in compiler optimization techniques over last few years?
8 votes

I suppose the Equality Saturation technique, as a different approach to the problem of optimization passes ordering, would be relevant. To my knowledge, it has however not yet been proved practical by ...

View answer
Conservative Approximation of Kleene-Mycroft Iteration for Polymorphic Recursion?
7 votes

You should have a look at the following paper -- and the previous work by Gori and Levi: On Polymorphic Recursion, Type Systems, and Abstract Interpretation Marco Comini, Ferruccio Damiani, Samuel ...

View answer
Implementing "Internal" Languages
Accepted answer
7 votes

In Extending Type Theory with Forcing by Guilhem Jaber, Nicolas Tabareau and Matthieu Sozeau, 2012, intuitionistic forcing is presented as an internalization of the presheaf construction, implemented ...

View answer
What are the negative consequences of extending CIC with axioms?
7 votes

One first reason to reject axioms is that they might be inconsistent. Even for the axioms that are proved consistent, some of them have a computational interpretation (we know how to extend ...

View answer
Is there a mathematical analysis/proof available for correctness of solutions to inter process communication problems?
7 votes

There has been various brand of work for formalizing such tricky code. The one I know about are (but I'm no expert on the topic): using "temporal logic" to study distributed systems; one important ...

View answer
Efficiently ordering typed programs
6 votes

Two remarks first: I have used the "randomly generate terms and check that they are well-typed" approach (you mention that "untyped" terms are generated, you can also randomly generate terms in a ...

View answer
How to specify and verify Horn clauses (logic programming programs)? Semantics of Horn clauses
Accepted answer
6 votes

You should have a look at Uniform Proofs as a Foudation for Logic Programming by Dale Miller, Gopalan Nadathur, Frank Pfenning and Andre Scedrov, 1991. The idea of this work and the rich area that has ...

View answer
What's the difference between reduction strategies and evaluation strategies?
6 votes

The "Reduction strategy" wikipedia article is entirely extracted out of a particular edit made by an anonymous IP to the "Evaluation strategy" article. The view that it represents is not consensual, ...

View answer
Which models of computation can be expressed through grammars?
6 votes

My answer is not intented to be formal, precise and absolutely in-topic. I think Marc Hamman's answer is rock solid, but your question made me think of a related topic. Grammars may be considered ...

View answer
Density of semantics in syntax
5 votes

Let's look at a simple example of a toy programming language with unary natural numbers and a "predecessor" operation. $$t ::= 0 \mid S~t \mid p~t$$ whose semantics is given by the following ...

View answer
Can concurrency models be compared in terms of some metrics?
5 votes

There are no metrics, but an excellent discussion of many concurrency models, in Tony Garnock-Jones PhD thesis. See the (HTML version of the) chapter "Approaches to coordination". This ...

View answer
How should I think about proof nets?
5 votes

There has been interesting work recently on making the relation between proof net and focused calculi tighter, using "multi-focused" variants where you may have several simultaneous left holes, and ...

View answer
Undecidability of program optimization
4 votes

Let fill be the Turing machine that writes 1 on all positions of its output tape (it doesn't terminate, but that's not an issue). Let now syra be the machine that computes the Syracuse/Collatz ...

View answer
Functions that typed lambda calculus cannot compute
4 votes

One vision of the limits of strongly normalizing calculi I like is the computability angle. In a strongly normalizing typed calculus, such as the core simply-typed lambda calculus, System F, or ...

View answer
Has anyone used Pottier and Gauthier's polymorphic defunctionalization in a modular compiler?
4 votes

Now, given their encoding, it's possible to add a catch-all case to their lambda datatype that isn't a tag, but which contains a higher-order function. This means that it should be possible to use ...

View answer
What's the logical counterpart to jumps with arguments on CPS terms?
3 votes

For me, what is going on is reasonably standard: You have $c$ with free variables $(x_i : \tau_i)_i$, and you replace it with $c[t_i/x_i]$ with the $(t_i)_i$ at types $(\tau_i)_i$; this is a standard ...

View answer
What does x.y notation mean?
Accepted answer
3 votes

This is the notation for Harper's "abstract binding structures": x.t represents the binding site of a variable x and the term t the variable scopes over. Apparently you are in the parts that ...

View answer
Modeling objects (OOP) in dependent type theory
2 votes

Why are you looking at dependent type theory to represent OOP? Can't we model OOP in a satisfying way with non-dependent calculi? I have an informal model of what OOP looks like, say, when translated ...

View answer