User Tools

Site Tools


projects:answerthesequestions

This is a list of questions that we've accumulated from Eugene, PLDI, etc. I feel like we should know the answer to these - at least enough to explain to someone else!

  • What is MinML?
  • What is higher-order abstract syntax?
  • What is a negative occurrence?
  • What is a Pi-type?
  • What is the Boyer-Moore school of theorem proving?
  • What did Tarski say about logic?
    • formula, interpretation –> either true or false?
  • What is the sequent calculus?
  • What is Godel's Completeness Theorem?
  • What is the Compactness Theorem?
  • What is the Lowenheim-Skolem Theorem?
  • What is Godel's First Incompleteness Theorem?
  • What is Godel's Second Incompleteness Theorem?
  • What is an incomputable function?
  • What is a primitive recursive function?
  • What is a general recursive function?
  • What is the axiom of choice?
  • What is the Curry-Howard isomorphism?
  • What is intuitionistic logic? Why is it so popular?
  • What are the ordinal numbers? Epsilon-0? Cardinal numbers? Formal numbers?
  • The ordinals are countable? Really?
  • Any termination argument can be embedded in ordinals?
  • What is term rewriting?
  • What is beta reduction? Eta expansion?
  • Linear ordering is different from well-founded ordering?
  • Epsilon-0 is well-founded?
  • What is Ackermann's function?
  • What is the Size Change Principle?
  • What is Barendregt's convention?
  • What is System F? What is its logical counterpart?
  • What is the lambda cube? What is its logical counterpart?
  • Explain how Hindley-Milner type inference works.
  • How is SMT-style logic and type-theory related? Is it?
  • What is a generalized algebraic data type?
  • What is a stack machine? CK machine?
  • What is the Metis theorem prover?
  • What is Spec#? How is it different from C#?
  • What is a partial command? Juno-2? LIM? (Greg Nelson)
  • What is the Galois connection between WLP and strongest postcondition?
  • How come no Galois connection with WP and anything else? No lower adjoint?
  • How does ESC/Java have unsound reasoning, while Spec# has sound reasoning?
  • What is abstract DPLL?
  • What is Algorithm W?
  • Why aren't mutable values in ML polymorphic?
  • What is CPS conversion, and why do it? (Danvy/Filinski)
  • What is closure conversion, and why do it? Lambda lifting? Hoisting?
    • (Appel's book)
  • When is a theory stably-infinite? Why is it important? What happens when it's not?
  • When is a theory convex? Why is it important? What happens when it's not?
  • Is there a mechanized proof of the correctness of the Nelson-Oppen procedure?
  • What is Houdini? How well does it work? Why isn't it used more often?
  • What is a dynamic frame? (Rustan)
  • What are frame axioms? (What didn't change?)
  • What is fluent calculus?
  • What is E-matching? (Simplify)
  • What is a trigger? (Simplify)
  • What is EPR theory?
  • What is PEX? (Microsoft Research)
  • Did Hoare really say in 2004 that types and assertions are redundant annotations?
  • Do we have a static way of reasoning about assertions written in temporal logic?
  • Do we have a mechanized way of reasoning about assertions written in TL?
  • Do we have a static way of reasoning about temporal properties?
  • What is linear logic?
  • What is dataflow?
    • Dataflow is a software architecture, where the idea is: If the value of variable A depends on the value of variable B, then if you change the value of B, the value of A is automatically recalculated.
    • Example: a spreadsheet program, where changing the value in a single cell will force recalculation of all dependent cells.
    • Why do it? Reduce amount of explicit dependency coupling in the code.
    • Also referred to as reactive programming.
    • Concurrency angle: Super-easy to program concurrent systems, because you don't have a global canonical view of the system - just of your own local node and the messages you receive. Often referred to as the counterpart to the von Neumann model of computation, where control flow is explicitly defined and data flow is implicit. Here, the control flow is implicit, where as the data flow is explicit. Currently these two models are viewed as two opposite extrema in the continuum of computer architecture designs (ref).
    • Sisal is a dataflow programming language. It kinda looks like C, but a variable can only be assigned to once.
    • Sooooo… Why isn't it used more widely?
      • Van Roy argues that the issue is more sociological than technical (ref). Finding enough parallelism in an imperative program is hard, and typically compilers are not up to the job. So people need to program in a dataflow paradigm, but that goes against standard practice.
      • Technically, two limitations seem to exist for dataflow parallel programs (ref). (1) Dataflow advocates say that it is easy to saturate the processors - simply add more threads. However synchronization/context switching cost is small only among a small number of threads, so as we scale up the number of threads, the latency induced by the sync cost starts to eat into maximum processor utilization rate. (2) Scheduling for dataflow architectures seems to have a static policy - jobs higher in the memory hierarchy are preferred. This local greedy strategy leads to un-optimal behavior.
  • What is the actor model?
  • How are dataflow model and actor model related?
  • How are dataflow model and hierarchical state machine model related?
  • What is a program dependence graph? parallel program graph?
  • What is the X10 programming language (IBM)?
  • What is Farka's Lemma?
  • What is refinement calculus? intuitionistic refinement calculus?
  • What is an abstract state machine? (Yuri Gurevich)
  • What is the zero-one law?
projects/answerthesequestions.txt · Last modified: 2009/02/24 15:58 (external edit)