longlivedeath + programming-languages-research   76

Note: Research
Papers that have had more or less influence on Rust, or which one might want to consult for inspiration or to understand Rust's background.
rust  programming-languages-research  papers  links 
august 2013 by longlivedeath
The HoTT Book | Homotopy Type Theory
Homotopy type theory is a new branch of mathematics that combines aspects of several different fields in a surprising way. It is based on a recently discovered connection between homotopy theory and type theory. It touches on topics as seemingly distant as the homotopy groups of spheres, the algorithms for type checking, and the definition of weak ∞-groupoids. Homotopy type theory offers a new “univalent” foundation of mathematics, in which a central role is played by Voevodsky’s univalence axiom and higher inductive types. The present book is intended as a first systematic exposition of the basics of univalent foundations, and a collection of examples of this new style of reasoning — but without requiring the reader to know or learn any formal logic, or to use any computer proof assistant. We believe that univalent foundations will eventually become a viable alternative to set theory as the “implicit foundation” for the unformalized mathematics done by most mathematicians.
programming-languages-research  homotopy-type-theory  type-theory 
june 2013 by longlivedeath
The Quipper Language
Quipper is an embedded, scalable functional programming language for quantum computing.
tolookat  programming-languages-research  quantum-computing 
june 2013 by longlivedeath
Type Systems for Modules (Winter 2010)
Module systems are central to the construction of large-scale programs, and there is a rich and highly-developed theory devoted to the study of type systems for modules. In this seminar course, we will focus attention on the origins, design, semantics and implementation of the ML module system, one of the most influential and highly evolved module systems available. We will investigate the numerous issues that arise in formalizing ML modules, as well as the different styles of formalization (e.g. ad-hoc, direct-style, elaboration), and we will also study a variety of challenging extensions to the ML module system, including higher-order functors and recursive modules.
module-systems  courses  programming-languages-research 
april 2011 by longlivedeath
Oregon Programming Languages Summer School
Видеоуроки по Coq (и сопутствующей теории).
videos  towatch  dependent-types  programming-languages-research 
january 2011 by longlivedeath
The Theory of Classification - A Course on OO Type Systems
A series on object-oriented type theory, aimed specifically at non-theoreticians.
type-theory  object-oriented  oop  programming-languages-research 
april 2010 by longlivedeath
TeaCODE.com - Библиотека
Имеются любопытные слайды от Roland Backhouse.
links  books  slides  computer-science  reference  programming-languages-research 
december 2008 by longlivedeath
Orc Language
Orc is a novel language for distributed and concurrent programming which provides uniform access to computational services, including distributed communication and data manipulation, through sites. Using three simple concurrency primitives, the programmer orchestrates the invocation of sites to achieve a goal, while managing timeouts, priorities, and failures.
concurrency  tolookat  programming-languages-research 
december 2008 by longlivedeath
Design Concepts in Programming Languages | Web Supplement | Home
MIT'овский учебник для аспирантов по языкам программирования.
books  computer-science  programming-languages-research 
december 2008 by longlivedeath
FP Lunch » Blog Archive » Call-by-push-value
[...] My motivation for this is very different from Paul Levy’s: I’m dreaming of a language with enough laziness to be interesting, but with more predictable memory usage than Haskell.
haskell  functional-programming  tolookat  programming-languages-research 
november 2008 by longlivedeath
OBJ Family: OBJ3 CafeOBJ Maude Kumo FOOPS Eqlog
"OBJ" refers to the language family, while "OBJ2," "OBJ3", "CafeOBJ," "BOBJ," etc. refer to particular members of the family. The OBJ languages are broad spectrum algebraic programming and specification languages, based on order sorted equational logic, possibly enriched with other logics (such as rewriting logic, hidden equational logic, or first order logic), and providing the powerful module system of parameterized programming.
functional-programming  obj  tolookat  research  computer-science  programming-languages-research 
september 2008 by longlivedeath
Lucid Synchrone
Lucid Synchrone is an experimental language for the implementation of reactive systems. It is based on the synchronous model of time as provided by Lustre combined with some features from ML languages.
functional-programming  lucid-synchrone  tolookat  research  computer-science  programming-languages-research 
september 2008 by longlivedeath
CHARITY - Home Page
Charity is a categorical programming language currently being developed by The Charity Development Group in The Department of Computer Science at The University of Calgary, Canada.
functional-programming  category-theory  tolookat  research  computer-science  charity  programming-languages-research 
september 2008 by longlivedeath
Bart Jacobs (Index)
Дядя пишет книгу про коалгебры и вообще много интересного пишет.
category-theory  computer-science  personal-pages  coalgebras  bart-jacobs  tolookat  programming-languages-research 
may 2008 by longlivedeath
Компьютерные науки и информационные технологии. Библиотека ЮрИнфоР
Походу единственное место на сети, где продаётся книжка Вольфенгагена про комбинаторную логику + кое-какие труды по теории категорий.
computer-science  category-theory  combinatory-logic  wolfengagen  toread  programming-languages-research 
may 2008 by longlivedeath
Room 101: Cutting out Static
Внятно обьясняет, почему статические переменные есть зло.
coding-standards  c++  design-patterns  static-variables  programming-languages-research 
february 2008 by longlivedeath

Copy this bookmark: