Dominic Mulligan
  • Member for 11 years, 5 months
  • Last seen more than 1 year ago
Major unsolved problems in theoretical computer science?
26 votes

I know the OP asked for only one problem per post, but the RTA (Rewriting Techniques and their Applications) 1 and TLCA (Typed Lambda Calculi and their Applications) conferences both maintain lists of ...

View answer
How do 'tactics' work in proof assistants?
15 votes

How do 'tactics' work in proof assistants? I suspect this answer will be a bit of a ramble. First, it isn't enough to ask "how tactics work in proof assistants" because they work differently in ...

View answer
Powerful Algorithms too complex to implement
13 votes

The linear time higher-order pattern unification algorithm by Qian has never been implemented due to its complexity AFAIK.

View answer
Are there any counterintuitive results in theoretical computer science?
13 votes

How about Martin Escardo's publications showing that there are infinite sets that can be exhaustively searched over in finite time? See Escardo's guest blog post on Andrej Bauer's blog, for instance, ...

View answer
Small steps for better TCS conferences?
12 votes

Reduce the number of sequential talks. Three half-hour highly technical talks following immediately after one another is hopeless. Nobody can concentrate for that long without a break. Ideally ...

View answer
Where and how did computers help prove a theorem?
12 votes

Christian Urban used the Isabelle proof assistant to check one of the main theorems in his PhD thesis was actually a theorem [1]. Using the assistant, a few changes needed to be made, but the result ...

View answer
What are possible implementations of Haskell's type classes and what are their (dis)advantages?
8 votes

JHC uses a different approach. The compiler's intermediate language is a dependently typed lambda-calculus where there is no distinction between types and values. JHC therefore can perform a case ...

View answer
Does the order of declarations in an inductive type matter?
7 votes

Does the order matter in the way you ask? No. But is the order completely irrelevant to the functioning of the proof assistant? Again, no. In Matita, a proof assistant very similar to Coq, the ...

View answer
Using lambda calculus to derive time complexity?
7 votes

You could also look up calculi of explicit substitutions which break up the meta-level substitution of the lambda-calculus into a series of explicit reduction steps. This touches on Charles' point ...

View answer
How would I go about learning the underlying theory of the Coq proof assistant?
6 votes

Luo's book on the Extended Calculus of Constructions is also a good reference. ECC was quite influential in the design of Coq's type theory.

View answer
Examples of "Unrelated" Mathematics Playing a Fundamental Role in TCS?
6 votes

This may or may not count, but recently Zermelo-Fraenkel with atoms (ZFA) and Fraenkel-Mostowski (FM) set theories have been applied to the study of abstract syntax with name binding. ZFA was ...

View answer
Proving running time upper bounds for algorithms in dependent type theory
4 votes

For verified complexity analysis in other theorem proving systems, see e.g. Tobias Nipkow's paper on this subject using the Isabelle theorem prover ("Amortised Complexity Verified" at ITP 2015) which ...

View answer
Purely Functional Equivalent of B-Tree?
4 votes

If you're interested in writing a purely functional database, you should probably check out Phil Trinder's PhD thesis which was on this very subject. He has a chapter on the use of B-Trees.

View answer
What is schema theory within Genetic Algorithms
Accepted answer
4 votes

If I remember correctly (it's years since I last studied this), schema theory isn't really used for anything. Rather, it's an attempt to explain why genetic algorithms seem to work well. As I'm not ...

View answer
Type systems preventing laziness-related memory leaks?
3 votes

Levy's call by push value calculus makes a distinction between values and their thunks. For a value v of type ty the computation thunk v has type U ty. Lindley and McBride's Frank language, inspired ...

View answer
Tool for specifying operational semantics for given formally specified programming language
3 votes

We have been working on one for the last few years: Lem, a higher-order, typed language with backends for OCaml, Coq, Isabelle/HOL, HOL4, LaTeX and HTML. Lem has been used internally in the group to ...

View answer
What is the state of the art in theory of "Software transformations preserving behavior"?
3 votes

I think what you are looking for, in the context of verified transformations in a proof assistant, is known as "refinement", wherein a very-high level, inefficient implementation of some algorithm is ...

View answer
Type inference for imperative statements other than assignment
3 votes

Xavier Leroy's PhD thesis is a good start.

View answer
finding constantness of a term
3 votes

You might want to take a look at the compiler literature for some ideas. What you're describing is akin to a well-known compiler optimization (virtually any modern compiler worth its salt will do it) ...

View answer
Monitoring PhD positions in TCS
2 votes

For type theory, the TYPES/announce mailing list appears to be the place where these are announced. There's also the LOGIC mailing list where theoretical jobs are announced in the German speaking ...

View answer