HackerPapers

arXiv:1307.5277cs.PL

Formalisation of the lambda aleph Runtime

Neal Glew, Tim Sweeney, Leaf Petersen

Early discovery. Linked by one identifiable commenter. This paper is outside the main ranking; a mention is not an endorsement.

Abstract

In previous work we describe a novel approach to dependent typing based on a multivalued term language. In this technical report we formalise the runtime, a kind of operational semantics, for that language. We describe a fairly comprehensive core language, and then give a small-step operational semantics based on an abstract machine. Errors are explicit in the semantics. We also prove several simple properties: that every non-terminated machine state steps to something and that reduction is deterministic once input is fixed.

arXiv comments
Journal reference
DOI
Subjects
cs.PLProgramming Languages

On Hacker News

Linked by 1 identifiable commenter in 1 comment across 1 thread, from Aug 2013 to Aug 2013.

Comments linking this paper, per year.

Discussed in comments1 thread

  1. John Carmack: Thoughts on Haskell [video] 1 comment

    • Tim Sweeney (Unreal Engine) has also written about haskell and specifically STM (http://www.st.cs.uni-saarland.de/edu/seminare/2005/advanced-...) and more recently on dependently typed languages (http://arxiv.org/pdf/1307.5277v1.pdf).

      sseveranView on HNParent context

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.