Posts By: Charles Stewart
| Date | Post | Topic |
| 05/21/2012 | Bounds on bounding | Encoding System Fw in predicative dependent type theory |
| 04/18/2012 | False dichotomy | Retrospective Thoughts on BitC |
| 04/18/2012 | Rust isn't GCed | Retrospective Thoughts on BitC |
| 02/09/2012 | Teaching challenge: culturally enriching formulae-as-types | Teaching challenge: culturally enriching formulae-as-types |
| 02/10/2012 | Too heavyweight | Teaching challenge: culturally enriching formulae-as-types |
| 01/30/2012 | What exactly can it do? | Vellvm: Formalizing the LLVM Intermediate Representation for Verified Program Transformations |
| 02/03/2012 | New England ++ | Vellvm: Formalizing the LLVM Intermediate Representation for Verified Program Transformations |
| 01/23/2012 | Beyond pure Prolog: Power and danger | Beyond pure Prolog: Power and danger |
| 12/16/2011 | Intuition deficit | What is this type of type called? |
| 12/16/2011 | Assumption discharged | What is this type of type called? |
| 12/16/2011 | Purpose | Designing a languge — what theory is a must? |
| 12/07/2011 | Restricting structural induction | Proofs of a type system's safety? |
| 11/14/2011 | LTL types FRP | LTL types FRP |
| 11/14/2011 | PLPV | LTL types FRP |
| 11/14/2011 | Oops | LTL types FRP |
| 11/16/2011 | Nice slides | LTL types FRP |
| 11/17/2011 | D4.3? | LTL types FRP |
| 11/18/2011 | D4.3 | LTL types FRP |
| 11/14/2011 | Who is confused? | math proofs are more robust than computer proofs |
| 11/14/2011 | There's proofs and proofs | math proofs are more robust than computer proofs |
| 01/24/2012 | Physical proofs and refutations | Foundations of Inference |
| 09/19/2011 | LtU always repeats itself four times | What Does Functional Programming Mean? |
| 09/12/2011 | The SAFE Platform | The SAFE Platform |
| 09/13/2011 | No virtual memory | The SAFE Platform |
| 09/09/2011 | Some old ones | What needs to be done? |
| 09/12/2011 | Tools | What needs to be done? |
| 09/15/2011 | What are iteratees? | What needs to be done? |
| 09/16/2011 | Underinformed speculation | What needs to be done? |
| 09/29/2011 | Feyerabend with focus | What needs to be done? |
| 09/09/2011 | The Trouble with Erlang | The Trouble with Erlang |
| 09/13/2011 | By general, you must understand we don't mean general | The Trouble with Erlang |
| 09/14/2011 | Really, really general purpose programming language | The Trouble with Erlang |
| 09/13/2011 | Does the post only feature weak arguments? | The Trouble with Erlang |
| 08/26/2011 | Old books are good | quite "old" books discussion |
| 08/29/2011 | Posterity | quite "old" books discussion |
| 08/30/2011 | Some old books are unread by me | quite "old" books discussion |
| 06/27/2011 | encourage an editor | Why Programming Languages? |
| 06/24/2011 | Miller vs Dybvig | The Value Of Syntax? |
| 06/15/2011 | Provable shrinkings | Catamorphisms and anamorphisms = general or primitive recursion? |
| 05/27/2011 | Might not be obvious how to apply this here | Yet another programming language with customizable syntax |
| 05/26/2011 | Ensure < is associative | Yet another programming language with customizable syntax |
| 05/26/2011 | Good catch | Yet another programming language with customizable syntax |
| 05/27/2011 | Particulars and patterns | Yet another programming language with customizable syntax |
| 05/18/2011 | Preprint | Artificial Grammar Reveals Inborn Language Sense |
| 05/19/2011 | Good link | Artificial Grammar Reveals Inborn Language Sense |
| 05/13/2011 | Are You Using the Right Axiomatic System? | Are You Using the Right Axiomatic System? |
| 05/05/2011 | Theory of descriptions | Enso: William Cook's new programming model |
| 05/02/2011 | Another question | Iteration function in lambda calculus |
| 05/02/2011 | Will do | Iteration function in lambda calculus |
| 05/03/2011 | Not what I'm after | Iteration function in lambda calculus |
| 05/03/2011 | Yes, nice | Iteration function in lambda calculus |
| 05/03/2011 | Right | Iteration function in lambda calculus |
| 05/05/2011 | The problematic, but not inferior, Church encoding | Iteration function in lambda calculus |
| 05/05/2011 | Counterexample accessed | Iteration function in lambda calculus |
| 05/06/2011 | Pseudo eta | Iteration function in lambda calculus |
| 04/24/2011 | Autonomous rational agents... | Elephants don't play chess |
| 04/20/2011 | The big change from r5rs | First draft of Scheme R7RS small language available |
| 04/21/2011 | (name) module procedure | First draft of Scheme R7RS small language available |
| 03/02/2011 | IEEE changes colour | IEEE changes colour |
| 03/02/2011 | Fixed | IEEE changes colour |
| 03/04/2011 | Embedability | Middle History of Logic Programming |
| 03/04/2011 | Haynes | Middle History of Logic Programming |
| 02/28/2011 | This is known as the 'Frame | Can contracts provide the features of type classes, bounded quantification and effect systems? |
| 02/16/2011 | CL packages | Extending Syntax from Within a Language |
| 12/20/2010 | STL, Haskell 98 | Interesting Standard Libraries to Study |
| 02/19/2011 | Coefficient of relevance | IBM's Watson plays Jeopardy champion Ken Jennings in February |
| 02/19/2011 | Web logic | IBM's Watson plays Jeopardy champion Ken Jennings in February |
| 10/28/2010 | Top-notch smartassery | The Myths of Object-Orientation |
| 10/28/2010 | Really? | The Myths of Object-Orientation |
| 10/25/2010 | IEEE | Languages with ANSI Standards |
| 10/26/2010 | It doesn't help all that much | Languages with ANSI Standards |
| 10/20/2010 | Is it really context sensitive? | another new language, Chomsky hierarchy Type-0 |
| 10/21/2010 | A can of worms | another new language, Chomsky hierarchy Type-0 |
| 10/24/2010 | Strengths of type safety | another new language, Chomsky hierarchy Type-0 |
| 11/03/2010 | Families of type-1 | another new language, Chomsky hierarchy Type-0 |
| 10/24/2010 | Three takes on the censure of features | another new language, Chomsky hierarchy Type-0 |
| 10/25/2010 | Political trichotomies | another new language, Chomsky hierarchy Type-0 |
| 10/27/2010 | What claims should be made about Ameba? | another new language, Chomsky hierarchy Type-0 |
| 10/28/2010 | Ameba's future | another new language, Chomsky hierarchy Type-0 |
| 10/29/2010 | Can of worms, revisited | another new language, Chomsky hierarchy Type-0 |
| 10/30/2010 | No | another new language, Chomsky hierarchy Type-0 |
| 11/03/2010 | Chomsky hierarchy considered of marginal interest | another new language, Chomsky hierarchy Type-0 |
| 10/29/2010 | Ameba fission | another new language, Chomsky hierarchy Type-0 |
| 10/05/2010 | Operating systems shouldn't be | Design Principles Behind Smalltalk |
| 10/06/2010 | The Tortoise and The Hare | Design Principles Behind Smalltalk |
| 10/07/2010 | Ropes the Ultimate | Design Principles Behind Smalltalk |
| 10/07/2010 | Mea Culpa | Design Principles Behind Smalltalk |
| 09/13/2010 | A month of implementation can easily save hours of debugging | Fortifying Macros |
| 09/15/2010 | Source transformations vs. source transformations | Fortifying Macros |
| 09/02/2010 | sci.lang FAQ #20: Is English a Creole? | Sapir-Whorf 70 years on |
| 09/03/2010 | Authorities can't always be so easily cited | Sapir-Whorf 70 years on |
| 08/30/2010 | Reference-centred discussion | Theoretical Computer Science StackExchange Beta now open |
| 08/11/2010 | Incentives | It's been ten years! |
| 07/15/2010 | Something I'm not getting | Generative Grammar-based Computation |
| 07/20/2010 | Very promising | Generative Grammar-based Computation |
| 05/08/2011 | Which models of computation can be expressed through grammars? | Generative Grammar-based Computation |
| 07/06/2010 | The spectrum of computational effects: two questions | Handlers of Algebraic Effects |
| 07/07/2010 | Thanks | Handlers of Algebraic Effects |
| 07/05/2010 | A most artistic package of a jumble of ideas | An intuitionistic logic that proves Markov's principle |
| 07/06/2010 | Origins and essence of Markov's principle | An intuitionistic logic that proves Markov's principle |
| 07/07/2010 | Stepwise decidability of halting | An intuitionistic logic that proves Markov's principle |
| 07/05/2010 | Two kinds of semantics | Evocative metaphor |
| 07/05/2010 | The Vienna Circle in lots of context | Evocative metaphor |
| 07/15/2010 | No place for academics | Why Undergraduates Should Learn the Principles of Programming Languages |
| 06/09/2010 | Why now? | Racket Released |
| 06/09/2010 | Right | Racket Released |
| 06/09/2010 | I read the explanation... | Racket Released |
| 06/09/2010 | Thanks | Racket Released |
| 06/12/2010 | Seems so | Data schema languages |
| 06/09/2010 | I guess... | The Resurgence of Parallelism |
| 05/27/2010 | There are no original ideas, only new accidents and mistakes | Alan Kay's 70th |
| 05/19/2010 | Mollom | The War on Spam |
| 05/17/2010 | Two questions | What's the name for this model of computation? |
| 05/17/2010 | Countability of sets of computations | What's the name for this model of computation? |
| 05/07/2010 | Spam filters | Spam filters |
| 05/08/2010 | Getting antond | Spam filters |
| 05/07/2010 | Three things | Code Quarterly - The Hackademic Journal |
| 05/07/2010 | Good | Code Quarterly - The Hackademic Journal |
| 05/08/2010 | ACM | Code Quarterly - The Hackademic Journal |
| 05/01/2010 | Can atoms be polymorphic? | Typed Lambda Calculus |
| 05/01/2010 | Schemes and polymorphism | Typed Lambda Calculus |
| 05/02/2010 | Encoding ML's let | Typed Lambda Calculus |
| 05/04/2010 | Hard-pressed encodings | Typed Lambda Calculus |
| 05/02/2010 | Meaningless "polymorphism" | Typed Lambda Calculus |
| 05/02/2010 | Definitions | Typed Lambda Calculus |
| 05/04/2010 | Barendregt on types | Typed Lambda Calculus |
| 05/05/2010 | Schematic polymorphism | Typed Lambda Calculus |
| 04/22/2010 | Get up and dance | SEC interested in formalising contracts ... in Python |
| 05/05/2010 | Double specification | SEC interested in formalising contracts ... in Python |
| 04/16/2010 | PLDI, POPL, ESOP | hot topics in type theorem |
| 04/16/2010 | Agile or steadfast? | How can C Programs be so Reliable? |
| 04/22/2010 | False dichotomy | How can C Programs be so Reliable? |
| 04/16/2010 | Wisdom | How can C Programs be so Reliable? |
| 04/05/2010 | Rerepresenting diagrams | A Formal System For Euclid's Elements |
| 04/05/2010 | Formal diagrammatic reasoning | A Formal System For Euclid's Elements |
| 04/01/2010 | Relevance logic | Incompleteness Theorems: The Logical Necessity of Inconsistency |
| 02/07/2012 | The popularity of Lua's FFI | Small is Beautiful: the design of Lua |
| 02/03/2012 | Dispensable fundamental notions | Small is Beautiful: the design of Lua |
| 02/07/2012 | Sequences and essentials | Small is Beautiful: the design of Lua |
| 03/28/2010 | Can functional programming be liberated from the von Neumann paradigm? | Can functional programming be liberated from the von Neumann paradigm? |
| 03/31/2010 | Bait and switch | Can functional programming be liberated from the von Neumann paradigm? |
| 03/31/2010 | Not anything as systematic as a benchmark | Can functional programming be liberated from the von Neumann paradigm? |
| 04/11/2010 | Bad monads | Can functional programming be liberated from the von Neumann paradigm? |
| 03/31/2010 | Report on the programming language Bill 2018 | Can functional programming be liberated from the von Neumann paradigm? |
| 04/01/2010 | Nothing new under the sun | Can functional programming be liberated from the von Neumann paradigm? |
| 03/29/2010 | Who are the EAPLS? | Will data-intensive computing revolutionize programming languages? |
| 02/16/2010 | I don't know... | Historical question |
| 02/16/2010 | You have me hunting | Historical question |
| 02/17/2010 | Wikipedia did better | Historical question |
| 02/10/2010 | Graphical notation | Alternatives to parentheses for grouping |
| 02/05/2010 | Madrid | Continuity Analysis of Programs |
| 02/04/2010 | Typing's fundamental restrictions | more consistent macros? |
| 01/06/2010 | Not similar | Colorful dominoes game hides an exercise in propositional logic |
| 12/18/2009 | Mix | An Innocent Model of Linear Logic |
| 12/18/2009 | Designs | An Innocent Model of Linear Logic |
| 12/16/2009 | Large-cardinal type theory | Naive Question? Definition of "Higher Order" |
| 12/16/2009 | Nth-order logic | Naive Question? Definition of "Higher Order" |
| 12/16/2009 | Right | Claiming Infinity |
| 12/16/2009 | A mini-review | Claiming Infinity |
| 12/16/2009 | Crank? | Claiming Infinity |
| 02/03/2010 | Rational exponential expressions | Claiming Infinity |
| 12/17/2009 | Crank-o-meter | Claiming Infinity |
| 12/16/2009 | Semantic TCO trouble | Why Object-Oriented Languages Need Tail Calls |
| 12/02/2009 | Big and small | Top rated programming conferences? |
| 11/19/2009 | Congratulations to the Scratch team | Scratch: Programming for All |
| 11/20/2009 | Measuring harm | Scratch: Programming for All |
| 11/23/2009 | Another possibility | Scratch: Programming for All |
| 11/16/2009 | Over the years | Bytecodes meet Combinators: invokedynamic on the JVM |
| 11/16/2009 | Pike is {sometimes,often} maddening... | Go or Unladen Swallow? |
| 11/19/2009 | Good question | Go or Unladen Swallow? |
| 11/16/2009 | Unevaluated languages | Go or Unladen Swallow? |
| 11/19/2009 | Apple's version of Objective | Go or Unladen Swallow? |
| 11/17/2009 | Lisp machines are a special case | Go or Unladen Swallow? |
| 11/18/2009 | Why LispM GC is special | Go or Unladen Swallow? |
| 11/19/2009 | Serious retro | Go or Unladen Swallow? |
| 11/20/2009 | Strongly equating | John Hughes on Erlang and Haskell |
| 11/11/2009 | Acknowledgement | Haskell Type Constraints Unleashed |
| 10/30/2009 | Reasoning about code | Liskov's list of papers |
| 10/29/2009 | Quibble | Literate Programming: Retrospect and Prospects |
| 10/28/2009 | Original article | Retrospective: An Axiomatic Basis for Computer Programming |
| 10/24/2009 | Important story | Design Patterns 15 Years Later: An Interview with Erich Gamma, Richard Helm, and Ralph Johnson |
| 10/22/2009 | Have your AHOS and eat HOAS too! | Have your AHOS and eat HOAS too! |
| 10/18/2009 | SLIB | meta-Scheme? |
| 10/19/2009 | Mapping sweet spots | meta-Scheme? |
| 10/20/2009 | Simplicity: MIT v. New Jersey | Lisps, First-Class Special Forms, Fexprs, The Kernel Programming Language |
| 10/20/2009 | Dynamic, staged computation | Lisps, First-Class Special Forms, Fexprs, The Kernel Programming Language |
| 10/18/2009 | Mixing macros and procedures | Lisps, First-Class Special Forms, Fexprs, The Kernel Programming Language |
| 10/20/2009 | First-class sell out | Lisps, First-Class Special Forms, Fexprs, The Kernel Programming Language |
| 10/20/2009 | Whose type system? Which extension language? | Lisps, First-Class Special Forms, Fexprs, The Kernel Programming Language |
| 10/22/2009 | Aha! | Lisps, First-Class Special Forms, Fexprs, The Kernel Programming Language |
| 10/22/2009 | No | Lisps, First-Class Special Forms, Fexprs, The Kernel Programming Language |
| 10/15/2009 | Paulson's Logic and Proof | Course in mathematical logic with applications to computer science |
| 10/15/2009 | Felleisen's pure scheme | Standard, simple subset of Scheme for experimentation? |
| 10/09/2009 | Refactoring | Haskell in the real world: writing a commercial program in Haskell |
| 10/03/2009 | HOAS, the very idea | A Type-theoretic Foundation for Programming with Higher-order Abstract Syntax and First-class Substitutions |
| 10/05/2009 | de-Bruijn-like approaches | A Type-theoretic Foundation for Programming with Higher-order Abstract Syntax and First-class Substitutions |
| 10/06/2009 | The monsters of HOAS | A Type-theoretic Foundation for Programming with Higher-order Abstract Syntax and First-class Substitutions |
| 10/03/2009 | A minimal explanation | A Type-theoretic Foundation for Programming with Higher-order Abstract Syntax and First-class Substitutions |
| 10/23/2009 | It exists | A Type-theoretic Foundation for Programming with Higher-order Abstract Syntax and First-class Substitutions |
| 09/30/2009 | Whew! | How to respect language styles while translating? |
| 09/27/2009 | Managing cognitive complexity | Why Pseudo-Code? |
| 09/27/2009 | Well... | Why Pseudo-Code? |
| 09/28/2009 | Communicating & reasoning | Why Pseudo-Code? |
| 09/28/2009 | Stumped | Why Pseudo-Code? |
| 09/27/2009 | Pseudo-code is code that is not machine code | Why Pseudo-Code? |
| 09/29/2009 | Another use case... | Why Pseudo-Code? |
| 09/25/2009 | Order-sorted algebras | Turning every module into a functor automatically? |
| 09/28/2009 | Item notation | Turning every module into a functor automatically? |
| 09/28/2009 | Link fixed | Turning every module into a functor automatically? |
| 09/29/2009 | It did | Turning every module into a functor automatically? |
| 08/24/2009 | Expressive Modes and Species of Language | Expressive Modes and Species of Language |
| 08/21/2009 | Message to LtU editors | Function Interface Models for Hardware Compilation |
| 08/21/2009 | Good | Scheme to be split into two languages |
| 08/21/2009 | Two questions about administration | Scheme to be split into two languages |
| 08/22/2009 | Thanks | Scheme to be split into two languages |
| 08/20/2009 | The linear bestiary of François Pottier | The linear bestiary of François Pottier |
| 08/21/2009 | I wish I had read it... | The linear bestiary of François Pottier |
| 08/19/2009 | Python's growth | something strange happened after implementing a first interpreter |
| 08/17/2009 | Interference per Reynolds | functions vs procedures.. |
| 08/19/2009 | Interference and argument order | functions vs procedures.. |
| 08/20/2009 | Analysis inside the implementation proper | functions vs procedures.. |
| 08/20/2009 | Once more | functions vs procedures.. |
| 08/20/2009 | Haven't looked at the paper yet | Observational Equality, Now! |
| 07/31/2009 | Language and style | Definition of Functional Programming Language |
| 07/24/2009 | Pure type systems | (Very) Simpleminded kind question |
| 07/24/2009 | ASCII 1, APL 0 | Resolved Debates in Syntax Design ? |
| 07/24/2009 | Fortress input encodings | Resolved Debates in Syntax Design ? |
| 07/19/2009 | Coq | Lambda Cube and programming languages |
| 07/18/2009 | Munkres' Topology | Munkres' Topology |
| 07/21/2009 | Not for me anymore | Munkres' Topology |
| 07/10/2009 | Arduino | Open Source for Hardware? |
| 07/09/2009 | VEX | Oh no! Animated Alligators! |
| 07/10/2009 | Not yet that I can see | Oh no! Animated Alligators! |
| 07/09/2009 | Nice talk titles | MitchFest 2009: Symposium in Honor of Mitchell Wand |
| 07/08/2009 | Programming Satan's Computer | Programming Satan's Computer |
| 07/07/2009 | Trade-offs with abstraction | Trade-offs with abstraction |
| 07/09/2009 | Yes, trade-offs | Trade-offs with abstraction |
| 07/08/2009 | I knew I shouldn't have... | Trade-offs with abstraction |
| 07/09/2009 | Layers | Trade-offs with abstraction |
| 07/03/2009 | Top group blog | Top 200 Blogs for Developers |
| 07/04/2009 | The demands of the audience | Top 200 Blogs for Developers |
| 07/05/2009 | Good point | Top 200 Blogs for Developers |
| 06/27/2009 | The halting semi-problem | Most powerful terminating semantics? |
| 06/27/2009 | Dead end | Most powerful terminating semantics? |
| 06/26/2009 | Strong theories | Most powerful terminating semantics? |
| 06/30/2009 | Boolean relation theory | Most powerful terminating semantics? |
| 06/26/2009 | Story | Most powerful terminating semantics? |
| 06/27/2009 | Basics: arithmetics and TMs | Most powerful terminating semantics? |
| 06/19/2009 | First-class macros | Fully-parameterized, first-class modules with hygienic macros |
| 06/19/2009 | Essence six years on, ten years on | SSA vs. CPS (and ANF?) |
| 06/23/2009 | Not all easy to get | SSA vs. CPS (and ANF?) |
| 06/19/2009 | Diagram | Peter Van Roy: Programming Paradigms for Dummies |
| 06/18/2009 | TeX seconded, PS | Perlis Languages |
| 06/18/2009 | Syntax-semantics separation | Perlis Languages |
| 06/18/2009 | The syntax-semantics grenade | Perlis Languages |
| 06/19/2009 | Imperative Prolog | Perlis Languages |
| 06/18/2009 | Assembler | Perlis Languages |
| 06/19/2009 | There's more | Perlis Languages |
| 06/18/2009 | /bin/sh | Perlis Languages |
| 06/19/2009 | Context | Perlis Languages |
| 06/18/2009 | Two relevant stories from the archives | Why a diagram is (sometimes) worth ten thousand words |
| 06/16/2009 | Definitely on topic | Pregel - Large Scale Graph Computing at Google |
| 06/17/2009 | Thanks each | Pregel - Large Scale Graph Computing at Google |
| 06/16/2009 | Sapir-Whorf | How Does Our Language Shape The Way We Think? |
| 06/16/2009 | Priming | How Does Our Language Shape The Way We Think? |
| 06/17/2009 | More | How Does Our Language Shape The Way We Think? |
| 06/18/2009 | Culture | How Does Our Language Shape The Way We Think? |
| 06/18/2009 | What priming isn't | How Does Our Language Shape The Way We Think? |
| 06/18/2009 | Two definitions of priming | How Does Our Language Shape The Way We Think? |
| 06/17/2009 | Definition of linguistic gender | How Does Our Language Shape The Way We Think? |
| 06/17/2009 | Scholars don't listen to each other | How Does Our Language Shape The Way We Think? |
| 06/18/2009 | Another way | How Does Our Language Shape The Way We Think? |
| 06/18/2009 | Bourgeois computer science | How Does Our Language Shape The Way We Think? |
| 06/23/2009 | Sharing is evil when done thoroughly | GRS vs LTRS |
| 06/24/2009 | Not quite a spiral | GRS vs LTRS |
| 06/12/2009 | Proof theory and PL semantics | Semantics: Logic vs. PL |
| 06/12/2009 | Well... | Semantics: Logic vs. PL |
| 06/12/2009 | Muddy waters | Semantics: Logic vs. PL |
| 06/18/2009 | Algebraic nature of proof theory | Semantics: Logic vs. PL |
| 06/18/2009 | Two T's | Semantics: Logic vs. PL |
| 06/18/2009 | Second try | Semantics: Logic vs. PL |
| 06/15/2009 | Excellent post | Semantics: Logic vs. PL |
| 06/18/2009 | Thanks & big steps | Semantics: Logic vs. PL |
| 06/18/2009 | Some transition systems are more equal than others | Semantics: Logic vs. PL |
| 06/18/2009 | Difference | Semantics: Logic vs. PL |
| 06/15/2009 | Categorical semantics of logic | Semantics: Logic vs. PL |
| 06/12/2009 | Topics on topic | Job trends |
| 06/15/2009 | Getting to know us | Job trends |
| 06/05/2009 | Lectures on Jacques Herbrand as a Logician | Lectures on Jacques Herbrand as a Logician |
| 06/11/2009 | Is Herbrand Logic Herbrand's logic? | Lectures on Jacques Herbrand as a Logician |
| 06/05/2009 | Contribution | Peter Landin |
| 09/25/2009 | Another sketch by Richard Bornat... | Peter Landin |
| 06/04/2009 | Resource Bounded Certification | Computing Needs Time |
| 05/14/2009 | Scientists [dagger] engineers | Why Did M.I.T. Switch from Scheme to Python? |
| 05/26/2009 | Delegation | Why Did M.I.T. Switch from Scheme to Python? |
| 05/06/2009 | Scott-Strachey | Right on! |
| 05/07/2009 | HCI-centrism | Right on! |
| 05/07/2009 | Linguistic turn | Right on! |
| 05/01/2009 | Knight's tour | Looking for list of programming problems to thoroughly test a language |
| 04/22/2009 | Andrej Bauer on PLD | Andrej Bauer on PLD |
| 04/22/2009 | Quibble: out-of-scope variables | Andrej Bauer on PLD |
| 04/24/2009 | Shallow issues | Andrej Bauer on PLD |
| 04/27/2009 | Degrees of oppression | Andrej Bauer on PLD |
| 03/23/2009 | Open access at MIT and Harvard | Open access at MIT and Harvard |
| 03/18/2009 | Marrying VMs | Marrying VMs |
| 03/20/2009 | Two replies to a reply *is* discussion | Marrying VMs |
| 03/29/2009 | Multiple VMs | Marrying VMs |
| 03/30/2009 | 1=1+2 | Marrying VMs |
| 03/13/2009 | Lawvere Theories and Monads | Lawvere Theories and Monads |
| 03/13/2009 | Speculations | Lawvere Theories and Monads |
| 03/23/2009 | Gentility and impurity | Lawvere Theories and Monads |
| 03/31/2010 | A jumping-off point for Lawvere theories | Lawvere Theories and Monads |
| 12/01/2009 | Right | Lawvere Theories and Monads |
| 03/13/2009 | Uneasy | Advantages of pointfree? |
| 03/13/2009 | STEPS | A Tiny Computer |
| 03/03/2009 | Timely thread | The Meta-LtU Thread |
| 03/04/2009 | Thanks | The Meta-LtU Thread |
| 03/05/2009 | That particular conversation | The Meta-LtU Thread |
| 03/05/2009 | A post | The Meta-LtU Thread |
| 03/08/2009 | Programming language design (PLD) | The Meta-LtU Thread |
| 02/12/2009 | Atkey on arrows | Parameterized Notions of Computation |
| 02/08/2009 | 800lb gorilla of logical strength | What is the dual of { } ? |
| 02/09/2009 | CIC & natural intuitions | What is the dual of { } ? |
| 02/11/2009 | Understanding mathematical structures | What is the dual of { } ? |
| 02/12/2009 | Moving from LtU | What is the dual of { } ? |
| 02/09/2009 | Sets of nats & intuitions again | What is the dual of { } ? |
| 02/02/2009 | A quibble from the ignorant | Ruling out nonsensical data type definitions |
| 01/20/2009 | Compile-time staging | Macro systems |
| 01/19/2009 | XMF stages parsing & execution | Macro systems |
| 01/19/2009 | REPLs, staging & compilation | Macro systems |
| 01/16/2009 | Impredicative Sigma quantification | On the Strength of Proof-Irrelevant Type Theories |
| 01/16/2009 | Static syntax | What Are The Resolved Debates in General Purpose Language Design? |
| 12/17/2008 | ? is a functor | Any problems with true union types if all values are tagged? (like in a dynamically typed system, Lisp, etc.) |
| 12/18/2008 | ? is a functor, if we interpret application correctly | Any problems with true union types if all values are tagged? (like in a dynamically typed system, Lisp, etc.) |
| 12/17/2008 | Parametricity | Any problems with true union types if all values are tagged? (like in a dynamically typed system, Lisp, etc.) |
| 12/16/2008 | Capabilities parallelism? | Practicality of Exclusively Compiler-Driven Unboxing |
| 12/01/2008 | Semantics of Idealised Algol | Remembering everything - a new(?) idea for a new PL |
| 11/26/2008 | Some | refereed journal with open access? |
| 11/27/2008 | Aiming low | refereed journal with open access? |
| 12/01/2008 | Pale green | refereed journal with open access? |
| 12/01/2008 | Dark green: IEEE & ACM | refereed journal with open access? |
| 11/24/2008 | Positive and negative subformulae | Non-standard type theories for FP |
| 11/24/2008 | Impossibly meaningful | Non-standard type theories for FP |
| 11/24/2008 | Types as programs | Non-standard type theories for FP |
| 11/24/2008 | Puzzled | Non-standard type theories for FP |
| 11/24/2008 | Question | Non-standard type theories for FP |
| 11/24/2008 | I'm out at sea | Non-standard type theories for FP |
| 11/24/2008 | Prenex forms for intuitionistic type theory | Non-standard type theories for FP |
| 11/24/2008 | Speculation | Non-standard type theories for FP |
| 11/25/2008 | Prenex intuitionistic logic is decidable | Non-standard type theories for FP |
| 11/26/2008 | Too much work | Non-standard type theories for FP |
| 11/18/2008 | Seems OK | SEP entry on Combinatory Logic |
| 11/18/2008 | Structural rules | SEP entry on Combinatory Logic |
| 11/09/2008 | Trivial? | β, η, ξ ⊢ α? |
| 11/09/2008 | The higher-order abbreviation of transitivity | β, η, ξ ⊢ α? |
| 11/09/2008 | Good | The Origins of the BitC Programming Language |
| 11/10/2008 | Commercial PLDI | The Origins of the BitC Programming Language |
| 11/10/2008 | Formal semantics | The Origins of the BitC Programming Language |
| 11/07/2008 | College Publications | College Publications |
| 11/08/2008 | Thanks | College Publications |
| 11/06/2008 | Kernel languages defined | Oz/K: A kernel language for component-based open programming |
| 11/07/2008 | Somehow haven't read CTM | Oz/K: A kernel language for component-based open programming |
| 11/05/2008 | Worthwhile idea | New Programming Language Idea |
| 11/05/2008 | Imperative program synthesis | New Programming Language Idea |
| 11/06/2008 | You're welcome | New Programming Language Idea |
| 06/27/2009 | The Concept of Termination in Functional Languages | Total functional language self interpreter? |
| 11/07/2008 | Picking nitpicknits | Total functional language self interpreter? |
| 11/04/2008 | Self-verifying theories | Total functional language self interpreter? |
| 11/05/2008 | Two notions of consistency | Total functional language self interpreter? |
| 11/05/2008 | Diagonalisation | Total functional language self interpreter? |
| 10/29/2008 | Try this | Declarative layout and/or UI languages? |
| 10/22/2008 | Fω^C: a symmetrically classical variant of System Fω | Fω^C: a symmetrically classical variant of System Fω |
| 10/23/2008 | OP? That'd be me... | Fω^C: a symmetrically classical variant of System Fω |
| 12/01/2008 | Sorry, missed marco's question | Fω^C: a symmetrically classical variant of System Fω |
| 10/24/2008 | Classical Logic and Computation ག | Fω^C: a symmetrically classical variant of System Fω |
| 12/01/2008 | APAL CL&C sequel | Fω^C: a symmetrically classical variant of System Fω |
| 10/22/2008 | Formulae-as-types for pattern matching | Multiple Dispatch in Practice |
| 10/20/2008 | Système fonctionnel? | F in System F |
| 10/16/2008 | Restricting functionals | In which sense Joy is functional? |
| 10/18/2008 | Finite-rank intersection types | In which sense Joy is functional? |
| 10/20/2008 | Properties of type systems | In which sense Joy is functional? |
| 10/16/2008 | Understanding stack manipulations | In which sense Joy is functional? |
| 10/14/2008 | Not full TCO | No more tail calls in Javascript? |
| 10/13/2008 | Infrastructure issues | On the (perceived) equivalence of static and dynamically typed reflective programming languages |
| 10/06/2008 | Packrat parsing | Parsing Expression Grammars |
| 10/06/2008 | Algorithm-oriented syntax design considered harmful | Parsing Expression Grammars |
| 10/08/2008 | What are formal languages for? | Parsing Expression Grammars |
| 10/07/2008 | Context-free graph grammars | Visual Programming Language Syntax Formalisms |
| 09/29/2008 | Maude | Help with Mixfix in Bison? |
| 09/30/2008 | Curiosity | Help with Mixfix in Bison? |
| 09/30/2008 | Asymmetric evolution | Help with Mixfix in Bison? |
| 09/30/2008 | Ideological | Help with Mixfix in Bison? |
| 09/30/2008 | Maude again | Help with Mixfix in Bison? |
| 09/30/2008 | Row polymorphism? | Help with N-Ary functions? |
| 09/29/2008 | Cons trees | Help with N-Ary functions? |
| 09/29/2008 | Why Reia? | Reia: Python/Ruby style language on top of Erlang |
| 10/02/2008 | Side effects and fault tolerance | Reia: Python/Ruby style language on top of Erlang |
| 10/06/2008 | The inscrutably non-local SSA construction algorithm | Reia: Python/Ruby style language on top of Erlang |
| 09/27/2008 | Complexity | Information regarding financial crisis |
| 02/12/2010 | Spam magnet | Information regarding financial crisis |
| 10/01/2008 | Ossification | Simon Peyton Jones Interview |
| 09/19/2008 | AgentSpeak(L): programming with beliefs, desires and intentions | AgentSpeak(L): programming with beliefs, desires and intentions |
| 09/19/2008 | Different language | AgentSpeak(L): programming with beliefs, desires and intentions |
| 09/19/2008 | Mea culpa | AgentSpeak(L): programming with beliefs, desires and intentions |
| 09/19/2008 | Toys | AgentSpeak(L): programming with beliefs, desires and intentions |
| 09/17/2008 | Gasbichler's modules | First-class Macros |
| 09/18/2008 | Static checks | First-class Macros |
| 09/12/2008 | David Turner's solution of the Hamming problem | Irresistible programs |
| 09/12/2008 | N-queens | Irresistible programs |
| 09/12/2008 | Sequence Program | Irresistible programs |
| 09/15/2008 | Functional difference lists | Irresistible programs |
| 09/16/2008 | Bresenham's line and circle plotting alorithms | Irresistible programs |
| 09/05/2008 | Compiler Validation through Program Analysis | Compiler Validation through Program Analysis |
| 09/05/2008 | Translation Validation | Compiler Validation through Program Analysis |
| 09/04/2008 | The hard problem trading systems solve... | Stock exchanges: language design aspect |
| 09/06/2008 | [OT] Dark pools | Stock exchanges: language design aspect |
| 09/03/2008 | dynamic-wind | Unchecked Exceptions can be Strictly More Powerful than Call/CC |
| 09/04/2008 | dynamic-wind and unwind-protect | Unchecked Exceptions can be Strictly More Powerful than Call/CC |
| 09/09/2008 | Will Clinger's two implementations | Unchecked Exceptions can be Strictly More Powerful than Call/CC |
| 09/02/2008 | Three things | Review of a potential pramming language: Lima |
| 09/01/2008 | Closures for C | Closures for C |
| 09/02/2008 | Moribund 'C | Closures for C |
| 09/02/2008 | Maybe | Closures for C |
| 09/03/2008 | Good call | Closures for C |
| 09/15/2008 | foo_closure | Closures for C |
| 08/28/2008 | Tools with latex | From Writing and Analysis to the Repository: Taking the Scholars' Perspective on Scholarly Archiving |
| 08/27/2008 | Prolog and Peirce | Haskell for AI? |
| 07/23/2008 | Practical Set Theory | Practical Set Theory |
| 07/24/2008 | Proofless text | Practical Set Theory |
| 07/25/2008 | Correction | Practical Set Theory |
| 07/25/2008 | A comparison of Mizar and Isar | Practical Set Theory |
| 07/24/2008 | Linearity and control flow | FP in D 2.0 |
| 07/22/2008 | Rants and bashing | Systems programming in languages other than C? |
| 07/17/2008 | The Development of Intuitionistic Logic | The Development of Intuitionistic Logic |
| 07/18/2008 | Intuitionistic model theory | The Development of Intuitionistic Logic |
| 07/21/2008 | Safe-for-space closure conversion | Practical Bits of Making a Compiler for a New Language |
| 07/17/2008 | Garbage collection | Practical Bits of Making a Compiler for a New Language |
| 07/18/2008 | Triggering GC | Practical Bits of Making a Compiler for a New Language |
| 07/21/2008 | (noalloc expr) | Practical Bits of Making a Compiler for a New Language |
| 07/17/2008 | Fundamental formalisms | Ada, the Ultimate Lambda? |
| 07/17/2008 | What is computation? | Ada, the Ultimate Lambda? |
| 07/10/2008 | Can reply to a post that one is previewing | Can reply to a post that one is previewing |
| 07/10/2008 | Somewhat disappointing discussion | Functional Netlists |
| 07/10/2008 | Geometry of Synthesis | Functional Netlists |
| 07/10/2008 | *delete* | Functional Netlists |
| 07/03/2008 | Cambridge Mathematics Laboratory | Request for participation |
| 06/20/2008 | Pure imperative programming | Pure imperative programming |
| 06/20/2008 | Admin: which department? | Pure imperative programming |
| 06/17/2008 | Don't know much about forex or trading systems... | Forex trading with functional programming |
| 06/18/2008 | Marketing is popular | Functional Programming in the ACM CS Curriculum |
| 06/17/2008 | Yet another purity post | Functional Programming in the ACM CS Curriculum |
| 06/05/2008 | Looks compelling | Applied Proof Theory: Proof Interpretations and their Use in Mathematics |
| 06/02/2008 | Not obviously important | Dead-end theorems |
| 06/03/2008 | Inferential impact analysis? | Dead-end theorems |
| 06/02/2008 | Puzzled by title | Types Considered Harmful |
| 05/27/2008 | Goguen school | Category theory in design |
| 05/08/2008 | Uniform provability | History of Logic Programming: What went wrong, What was done about it, and What it might mean for the future |
| 05/08/2008 | LP vs FP | History of Logic Programming: What went wrong, What was done about it, and What it might mean for the future |
| 05/08/2008 | He's wrong | History of Logic Programming: What went wrong, What was done about it, and What it might mean for the future |
| 05/08/2008 | Towards a WAM Model for Lambda Prolog | History of Logic Programming: What went wrong, What was done about it, and What it might mean for the future |
| 05/15/2008 | A Treatment of Higher-order Features in Logic Programming | History of Logic Programming: What went wrong, What was done about it, and What it might mean for the future |
| 05/05/2008 | Arrows generalise monads and idioms | Arrows generalise monads and idioms |
| 05/07/2008 | Two counter clarifications | Arrows generalise monads and idioms |
| 04/29/2008 | Automatic Patch-Based Exploit Generation | Automatic Patch-Based Exploit Generation |
| 04/26/2008 | Goto considered harmful | Is Halting Problem Valid for P? |
| 04/26/2008 | What does the introductory course aim to teach? | 2nd Revision of "Thoughts about the Best Introductory Language" |
| 04/26/2008 | Logo's mindshare | 2nd Revision of "Thoughts about the Best Introductory Language" |
| 04/25/2008 | Andrew Pitts' work on OpSem... | On Presenting Operational Semantics |
| 04/23/2008 | *deleted* | program verification: the very idea |
| 04/23/2008 | Simplistic AI culture | program verification: the very idea |
| 04/23/2008 | Transputer | program verification: the very idea |
| 04/24/2008 | Thanks, CG&R | program verification: the very idea |
| 09/30/2008 | Verification methodology | program verification: the very idea |
| 04/21/2008 | No discussion of FCP | FPH: First-class Polymorphism for Haskell |
| 04/21/2008 | Theorem 4 | FPH: First-class Polymorphism for Haskell |
| 04/16/2008 | Whacky scoping? | Fan Programming Language |
| 04/16/2008 | Source | Fan Programming Language |
| 04/16/2008 | Not exactly | Fan Programming Language |
| 04/15/2008 | The irreducible physicality of security properties | The irreducible physicality of security properties |
| 04/16/2008 | Stung into sloganising | The irreducible physicality of security properties |
| 04/16/2008 | Impressed | The irreducible physicality of security properties |
| 04/17/2008 | Poor little number theorists | The irreducible physicality of security properties |
| 04/17/2008 | AI culture | The irreducible physicality of security properties |
| 04/16/2008 | From ambients to SElinux | The irreducible physicality of security properties |
| 04/17/2008 | Applications of ambients | The irreducible physicality of security properties |
| 04/16/2008 | Two thoughts | The irreducible physicality of security properties |
| 04/17/2008 | Scaling R&R | The irreducible physicality of security properties |
| 04/22/2008 | R&R and R&W and AAR&R | The irreducible physicality of security properties |
| 04/14/2008 | Evaluating PhD programs | Career paths and concerns |
| 04/18/2008 | Two BitC resources here | Career paths and concerns |
| 04/13/2008 | An approach to the de Bruijn criterion | Applications of formal semantics |
| 04/11/2008 | Mechanizing the Metatheory of LF | Mechanizing the Metatheory of LF |
| 04/13/2008 | Mea culpa | Mechanizing the Metatheory of LF |
| 04/10/2008 | Picture Languages | Context free grammar for shapes in a 2d grid? |
| 04/11/2008 | Applications of tree grammars | Context free grammar for shapes in a 2d grid? |
| 04/11/2008 | naasking wrote: I don't know | Safe and Secure Software in Ada |
| 04/13/2008 | TEMPEST | Safe and Secure Software in Ada |
| 04/13/2008 | Higher-order reasoning | Safe and Secure Software in Ada |
| 04/08/2008 | What is proven? | Proving compositions |
| 04/07/2008 | Where do low-level macro facilities hide? | Scheme macro systems |
| 04/07/2008 | Twelf | Rewriting rules for deducing properties of functions |
| 03/31/2008 | Or even... | Algebraist Network |
| 03/25/2008 | Rewriting logic | Dependent Types, Generic Programming and Overloading. |
| 03/31/2008 | To JVM | CERT C Secure Coding Standard |
| 03/28/2008 | Audit | CERT C Secure Coding Standard |
| 03/20/2008 | p9 | STEPS Toward The Reinvention of Programming: First Year Progress Report |
| 03/20/2008 | Alan Kayish ideas | STEPS Toward The Reinvention of Programming: First Year Progress Report |
| 03/25/2008 | There are a lot of achievements in the paper, but... | STEPS Toward The Reinvention of Programming: First Year Progress Report |
| 03/25/2008 | Coke and pre-scheme | STEPS Toward The Reinvention of Programming: First Year Progress Report |
| 03/13/2009 | Link broken | STEPS Toward The Reinvention of Programming: First Year Progress Report |
| 03/19/2008 | Games and regions | Eriskay: a Programming Language Based on Game Semantics |
| 03/19/2008 | Patience | Eriskay: a Programming Language Based on Game Semantics |
| 03/26/2008 | Eriskay: a Programming Language Based on Game Semantics | |
| 07/23/2008 | The compiler's promise | Is null needed? |
| 02/27/2008 | Backtracking arithmetic in Prolog | Pure, Declarative, and Constructive Arithmetic Relations |
| 02/27/2008 | Pure, Declarative, and Constructive Arithmetic Relations | Pure, Declarative, and Constructive Arithmetic Relations |
| 02/29/2008 | Purity and Presburger | Pure, Declarative, and Constructive Arithmetic Relations |
| 05/27/2008 | Unix programming exposed | succinctness |
| 02/01/2008 | Alpha conversion | Barendregt's Convention |
| 02/01/2008 | Which rule? | Barendregt's Convention |
| 01/30/2008 | Spec | Arc is released |
| 01/30/2008 | No hygiene | Arc is released |
| 01/31/2008 | James' definition of hygiene | Arc is released |
| 01/31/2008 | PG on hygiene | Arc is released |
| 02/26/2008 | Inertia | Arc is released |
| 01/28/2008 | Link | A Model for Formal Parametric Polymorphism: A PER Interpretation for System R |
| 01/28/2008 | Scala seems to do OK | VM's... What's the best? |
| 01/28/2008 | s48vm | VM's... What's the best? |
| 01/28/2008 | Value of the paper | Axioms and Theorems for a Theory of Arrays |
| 01/29/2008 | Still need test for object identity | Really un-mutable Scheme |
| 01/28/2008 | Cyclic data structures | Really un-mutable Scheme |
| 01/28/2008 | PLT supports immutable cyclic data structures | Really un-mutable Scheme |
| 01/25/2008 | An ignorant question about Erlang's type safety | How useful is reflection, anyway? |
| 01/26/2008 | Closure trouble | How useful is reflection, anyway? |
| 01/08/2008 | Authors | Call-by-value Termination in the Untyped Lambda-calculus |
| 01/08/2008 | JH said:As Perlis once | Computer Science Education: Where Are the Software Engineers of Tomorrow? |
| 12/13/2007 | Interest and resources | CUFP write-up |
| 12/11/2007 | S has a left inverse | S has a left inverse |
| 12/11/2007 | Comment #1: invertability | S has a left inverse |
| 12/12/2007 | S does not have a right inverse... | S has a left inverse |
| 12/11/2007 | Combinatory algebra | functions, statements, expressions |
| 12/07/2007 | In particular... | How to write your next POPL paper in Coq |
| 12/07/2007 | Thinking About Logic | Logic for Philosophy |
| 12/11/2007 | No, but... | Logic for Philosophy |
| 01/28/2008 | Good call | Logic for Philosophy |
| 11/12/2007 | CSLI lecture notes made freely available | CSLI lecture notes made freely available |
| 11/12/2007 | Intersection types | Universal Type System |
| 10/17/2007 | Still true? | Examples of large-scale functional language projects |
| 10/15/2007 | Formal science, natural computation | Computing is a Natural Science |
| 09/23/2007 | PEPM | Which Journals/Conferences to keep track of? |
| 09/07/2007 | Seconded | Examples of Categorical Semantics for Languages with Dependent Types |
| 09/01/2007 | I came to the same conclusion... | Escape from Zurg: An Exercise in Logic Programming |
| 09/03/2007 | Hacking Prolog | Escape from Zurg: An Exercise in Logic Programming |
| 08/29/2007 | Oh indeed! | Barker & Szabolcsi: New directions for proof theory in linguistics |
| 08/29/2007 | and also... | R6RS Validated |
| 08/30/2007 | rrrs-editors | R6RS Validated |
| 08/30/2007 | Indeed | What is a state? |
| 04/09/2008 | CHR survey MkII | Theory and Practice of Constraint Handling Rules |
| 05/13/2008 | Sorry! | Theory and Practice of Constraint Handling Rules |
| 08/23/2007 | Reasoning about code graphs | Declarative Assembler |
| 07/19/2009 | Some links | First-class Polymorphism |
| 08/03/2007 | Good question | Syntactic abstraction? (newbie question) |
| 08/03/2007 | Confused | Syntactic abstraction? (newbie question) |
| 07/12/2007 | Gandy's Principles for Mechanisms | A Natural Axiomatization of Church's Thesis |
| 07/16/2007 | Set theory in sheep's clothing | A Natural Axiomatization of Church's Thesis |
| 07/17/2007 | SOL | A Natural Axiomatization of Church's Thesis |
| 07/12/2007 | Thyer's DPhil & the efficiency of optimality | Lambda Animator |
| 07/09/2007 | Theorem proving support in programming language semantics | Theorem proving support in programming language semantics |
| 07/03/2007 | Clean & term graph rewriting | Q tutorial |
| 06/23/2009 | Plump's handbook article available | Q tutorial |
| 07/03/2007 | Two guesses | Forth in hardware ("not dead yet") |
| 07/05/2007 | The unbearable lightness of type-checking | Forth in hardware ("not dead yet") |
| 06/21/2007 | FIG & s48 | Application-specific foreign-interface generation |
| 06/22/2007 | What does the backend do? | Application-specific foreign-interface generation |
| 06/15/2007 | *scrub* | Carnap Programming Language |
| 06/05/2007 | Not sure | Typed callcc in a stack-based language |
| 05/24/2007 | Synthetic Computability | Synthetic Computability |
| 05/24/2007 | Iteration #2 | Synthetic Computability |
| 05/24/2007 | Wadler on Girard-Reynolds... | Festschrift for John C Reynolds's 70th Birthday |
| 05/25/2007 | Combining algebraic effects with continuations | Festschrift for John C Reynolds's 70th Birthday |
| 06/15/2007 | Core algebra revisited | Festschrift for John C Reynolds's 70th Birthday |
| 05/23/2007 | "Proof as program" analogy & fitting the formal to intuition | Social Processes and Proofs of Theorems and Programs |
| 05/24/2007 | Right, so far as it goes | Social Processes and Proofs of Theorems and Programs |
| 05/24/2007 | OCC - An Open Calculus of Constructions | Social Processes and Proofs of Theorems and Programs |
| 05/24/2007 | Quite! | Social Processes and Proofs of Theorems and Programs |
| 05/09/2007 | "The language of the future is javascript" | "The language of the future is javascript" |
| 06/15/2007 | Small is Beautiful, Large is Useful, and Scheme is Both | The PLT Scheme weblog |
| 04/23/2007 | Z & Prolog | Why is there not a PL with a mathematical type system? |
| 04/20/2007 | Light Logics and Optimal Reduction | Light Logics and Optimal Reduction |
| 04/24/2007 | Limited scope | Light Logics and Optimal Reduction |
| 04/24/2007 | Quibble | Church's Thesis and Functional Programming |
| 04/14/2007 | PCF and LCF | PCF and LCF |
| 04/17/2007 | Stanford LCF | PCF and LCF |
| 06/09/2011 | LCF ur-manuscript... | PCF and LCF |
| 03/15/2007 | Context logic & term rewriting, and bunched implication too | Separation Logic courses (Reynolds) |
| 03/15/2007 | Context Logic as Modal Logic | Separation Logic courses (Reynolds) |
| 03/06/2007 | Or maybe | Dao, a new programming language |
| 03/08/2007 | Thanks! | Dao, a new programming language |
| 02/07/2007 | Very nice | State of the Union: Type Inference via Craig Interpolation |
| 02/10/2007 | Standard proof theory | State of the Union: Type Inference via Craig Interpolation |
| 06/12/2007 | Dropping state on the floor | Steps Toward The Reinvention of Programming |
| 06/12/2007 | Thanks for the comments | Steps Toward The Reinvention of Programming |
| 01/16/2007 | Obligatory links | Beauty in the Beast |
| 01/04/2007 | 2 thoughts | Can referential transparency be bad? (puzzle included) |
| 01/05/2007 | not so strange | Can referential transparency be bad? (puzzle included) |
| 01/26/2008 | Nonsense with equations | Derivatives and dissections of data types |
| 01/05/2007 | Evidence from linguistics | Why numbering should start at 0 |
| 01/04/2007 | Sharing graphs and bigraphs | Quotation and evaluation -- or, how pure is the pure lambda calculus? |
| 12/08/2006 | Avoid Pelletier | Natural Deduction Reading for Beginners |
| 09/17/2008 | Java+ITP and the Key project | Typing a function which includes its axioms? |
| 11/01/2006 | Process calculi for transactions | Process calculi for transactions |
| 11/01/2006 | Links | Process calculi for transactions |
| 11/02/2006 | Thanks, good link | Process calculi for transactions |
| 02/05/2009 | Subjective impression | Process calculi for transactions |
| 02/05/2009 | Clinger on Actors & CSP | Process calculi for transactions |
| 10/10/2006 | Goedel-Loeb logic | A Very Modal Model of a Modern, Major, General Type System |
| 05/07/2008 | What is a Categorical Model of Arrows? | Arrows, like Monads, are Monoids |
| 01/05/2007 | In lieu of a review... | Lectures on the Curry-Howard Isomorphism |
| 01/16/2007 | Thanks | Lectures on the Curry-Howard Isomorphism |
| 04/13/2006 | Quote from Gilad | Flexible Addition of Static Typing to Dynamically Typed Programs |
| 03/30/2006 | Uniform Proofs as a Foundation for Logic Programming | Uniform Proofs as a Foundation for Logic Programming |
| 03/31/2006 | Resource predictability | Uniform Proofs as a Foundation for Logic Programming |
| 03/30/2006 | Chronology | Transactional Memory with data invariants (draft sequel to the STM-Haskell paper) |
| 03/30/2006 | Big fragment, little fragment | Class hierarchies and Ontologies |
| 03/30/2006 | I agree with neelk, more or less | Class hierarchies and Ontologies |
| 03/26/2006 | I'm moving... | Contributing Editors? |
| 03/10/2006 | No magic bullet | Visualisable Languages |
| 03/22/2006 | ACL2 ག | ACL2 in DrScheme |
| 03/10/2006 | syntax-case and s48ish modules | Scheme Language Steering Committee Report to the Community |
| 03/03/2006 | Towards Applicative Relational Programming | Towards Applicative Relational Programming |
| 03/03/2006 | Fixed | Towards Applicative Relational Programming |
| 03/03/2006 | Kent Pitman's remark | A Tail-Recursive Machine with Stack Inspection |
| 03/06/2006 | Thanks! | A Tail-Recursive Machine with Stack Inspection |
| 02/18/2006 | Gabriel & Steele | Accidental Syntax |
| 02/13/2006 | Better terminology | Type theory question... |
| 02/15/2006 | Fair enough | Type theory question... |
| 02/22/2006 | Sources | Type theory question... |
| 02/22/2006 | Distinction | Type theory question... |
| 02/23/2006 | Misled by whom? | Type theory question... |
| 02/03/2006 | Combinators for contracts | Combinators for contracts |
| 03/27/2009 | Document assembly | Combinators for contracts |
| 04/15/2010 | 30 common patterns | Combinators for contracts |
| 04/16/2010 | Relevance of contract typology | Combinators for contracts |
| 04/16/2010 | Ah, oh, I see | Combinators for contracts |
| 02/01/2006 | Data types and computation types | What is a monad, why should I use it, and when is it appropriate? |
| 02/02/2006 | No, not really | What is a monad, why should I use it, and when is it appropriate? |
| 01/26/2006 | Rho calculus | Rho calculus |
| 02/03/2006 | My interest | Rho calculus |
| 01/26/2006 | Propositions and identity | What is a Proposition? |
| 02/03/2006 | Yep | What is a Proposition? |
| 01/18/2006 | Double-edged macros | Lisp is sin |
| 01/17/2006 | Programming a compiler with a proof assistant | Programming a compiler with a proof assistant |
| 01/18/2006 | Non-obvious choices of PL for teaching | GAWK (GNU AWK) for AI? |
| 06/19/2008 | Build a block | New language for kids: Scratch - Logo meets Squeak Smalltalk? |
| 06/20/2008 | Not news | New language for kids: Scratch - Logo meets Squeak Smalltalk? |
| 01/18/2006 | Occam? | Guy Steele on Language Design |
| 01/18/2006 | Thanks | Guy Steele on Language Design |
| 12/15/2005 | Not much comment... | Frege's Contribution to Philosophy of Language |
| 11/02/2005 | WP links | Geometric Algebra |
| 11/02/2005 | Both sum type former and logical disjunction are inclusive or | Curry/Howard and Disjunction |
| 11/01/2005 | Linearity | Parsing and syntax reordering |
| 11/02/2005 | Foote's remark | OOPSLA 2005 Reports |
| 11/02/2005 | Still standing | OOPSLA 2005 Reports |
| 11/03/2005 | More Foote | OOPSLA 2005 Reports |
| 10/27/2005 | Well there isn't much written explicitly about the link... | Just What is it that Makes Martin-Lof's Type Theory so Different, so Appealing? |
| 10/27/2005 | PS: Greg Restall | Just What is it that Makes Martin-Lof's Type Theory so Different, so Appealing? |
| 10/31/2005 | Option (1) is spot on | Just What is it that Makes Martin-Lof's Type Theory so Different, so Appealing? |
| 10/31/2005 | neelk wrote: I'm pretty sure | Just What is it that Makes Martin-Lof's Type Theory so Different, so Appealing? |
| 11/01/2005 | WF types | Just What is it that Makes Martin-Lof's Type Theory so Different, so Appealing? |
| 10/25/2005 | Journal "Logical Methods in CS" | Journal "Logical Methods in CS" |
| 10/27/2005 | Typesafe general recursion | Journal "Logical Methods in CS" |
| 10/26/2005 | Depth notwithstanding... | Journal "Logical Methods in CS" |
| 04/11/2008 | Article | Mechanizing Language Definitions |
| 03/13/2009 | Link broken | Combining computational effects |
| 09/27/2005 | Eliminate threads & FAQ | LtU: Style and Focus |
| 09/22/2005 | Since we're talking about ruby... | Ruby: Language of the Programming Übermensch? |
| 09/20/2005 | FP without closures | Most Productive FP Lang? |
| 07/14/2008 | Reverse application and the lambda-calculus | Let's make a programming language! |
| 07/16/2008 | Yes, quite similar | Let's make a programming language! |
| 09/12/2008 | Frank's underspecified problem | Let's make a programming language! |
| 05/24/2007 | The Goal! | Don Box: Teaching my kids to program |
| 05/24/2007 | !?!APL | Don Box: Teaching my kids to program |
| 10/07/2005 | I missed this... | Ian Bicking: The challenge of metaprogramming |
| 03/03/2006 | Completely wrong? | Ian Bicking: The challenge of metaprogramming |
| 03/06/2006 | I was, in fact, completely wrong | Ian Bicking: The challenge of metaprogramming |
| 11/17/2009 | Definitely front page material | The Memory Pool System: Thirty person-years of memory management development goes Open Source |
| 11/07/2008 | Functional Programming and the J Programming Language | Dr. Kenneth Iverson Passes Away |
| 04/05/2005 | If fast-startup is your problem... | newLisp: A better Lisp/Scheme Fusion... |
| 06/26/2009 | Origins of message passing | Alan Kay: The Early History of Smalltalk |
| 01/19/2012 | In defence of cut, or in search of alternatives | Embedding Prolog in Haskell |
| 01/23/2012 | Intended semantics | Embedding Prolog in Haskell |
| 01/24/2012 | Equational logic is expensive | Embedding Prolog in Haskell |
| 01/24/2012 | Indeed | Embedding Prolog in Haskell |
| 01/25/2012 | Vulgar proof theory | Embedding Prolog in Haskell |
| 02/08/2012 | An error of perspective | Embedding Prolog in Haskell |
| LtU Topic Index Sorted by Date | LtU Topic Index Sorted by Topic | LtU Index of Post Authors | Zipped LtU Archive |