程式語言理論 - 第一階段調查

[nanchenchen]

第一階段目標：領域的初始探索 這個領域大致在做些什麼？可以舉幾個例子嗎？這個領域還分為什麼子領域(至少舉三個，並做簡單介紹)？

將查到的資料貼過來這裡(或是將自己知道的資訊寫下來)，要註明出處

最後整理成一個新的github wiki頁面到這個group的wiki

期限是4/19

[shhyou]

不好意思, 請問我能延後一週繳交嗎? 剛好 4/18 要考托福 T_T

[nanchenchen]

Okok 2015年4月7日 下午9:10 於 "suhorng" notifications@github.com 寫道：

不好意思, 請問我能延後一週繳交嗎? 剛好 4/18 要考托福 T_T

— Reply to this email directly or view it on GitHub https://github.com/tw-sparrowflying/field-investigation-group/issues/6#issuecomment-90797970 .

[shhyou]

Scope of Related Conferences

International Conference on Functional Programming (ACM SIGPLAN ICFP)

ICFP seeks original papers on the art and science of functional programming. Submissions are invited on all topics from principles to practice, from foundations to features, from abstraction to application. The scope includes all languages that encourage functional programming, including both purely applicative and imperative languages, as well as languages with objects or concurrency. Particular topics of interest include:

• Link to ICFP home page
• Language Design: type systems; concurrency and distribution; modules; components and composition; metaprogramming; relations to object-oriented or logic programming; interoperability
• Implementation: abstract machines; compilation; compile-time and run-time optimization; memory management; multi-threading; exploiting parallel hardware; interfaces to foreign functions, services, components or low-level machine resources
• Software-Development Techniques: algorithms and data structures; design patterns; specification; verification; validation; proof assistants; debugging; testing; tracing; profiling
• Foundations: formal semantics; lambda calculus; rewriting; type theory; monads; continuations; control; state; effects
• Transformation and Analysis: abstract interpretation; partial evaluation; program transformation; program calculation; program proof
• Applications and Domain-Specific Languages: symbolic computing; formal-methods tools; artificial intelligence; systems programming; distributed-systems and web programming; hardware design; databases; XML processing; scientific and numerical computing; graphical user interfaces; multimedia programming; scripting; system administration; security; education
• Functional Pearls: elegant, instructive, and fun essays on functional programming

Principles of Programming Languages (ACM SIGPLAN POPL)

The annual Symposium on Principles of Programming Languages is a forum for the discussion of all aspects of programming languages and systems, with emphasis on how principles underpin practice. Both theoretical and experimental papers are welcome, on topics ranging from formal frameworks to experience reports. Papers discussing new ideas and areas are most welcome, as are high-quality expositions or elucidations of existing concepts that are likely to yield new insights ("pearls").

• ACM SIGPLAN POPL

Programming Language Design and Implementation (ACM SIGPLAN PLDI)

About/ PLDI is a premier forum for all areas of programming language research, including the design, implementation, theory, and efficient use of languages. PLDI’s emphases include innovative and creative approaches to compile-time and runtime technology, novel language designs and features, and results from implementations.

Call for Papers 2014/ PLDI is a forum for the exchange of information on programming languages, their design, implementation, development, and use. PLDI emphasizes innovative and creative approaches to compile-time and runtime technology, novel language designs and features, and results from implementations.

• Link to 2014 PLDI
• Language designs and extensions
• Static and dynamic analysis of programs
• Domain-specific languages and tools
• Type systems and program logics
• Program transformation and optimization
• Checking or improving the security or correctness of programs
• Memory management
• Parallelism, both implicit and explicit
• Performance analysis, evaluation, and tools
• Novel programming models
• Debugging techniques and tools
• Program understanding
• Interaction of compilers/runtimes with underlying systems
• Program synthesis

Asian Symposium on Programming Languages and Systems (APLAS)

About/ APLAS aims to stimulate programming language research by providing a forum for the presentation of latest results and the exchange of ideas in programming languages and systems. APLAS is based in Asia, but is an international forum that serves the worldwide programming language community.

Topics/ The symposium is devoted to foundational and practical issues in programming languages and systems.

• APLAS 2015 Home Page
• semantics, logics, foundational theory
• design of languages, type systems and foundational calculi
• domain-specific languages
• compilers, interpreters, abstract machines
• program derivation, synthesis and transformation
• program analysis, verification, model-checking
• logic, constraint, probabilistic and quantum programming
• software security
• concurrency and parallelism
• tools and environments for programming and implementation

[shhyou]

Some Good Textbooks

Types and Programming Languages

• Author: Benjamin C. Pierce / The MIT Press
• Category: Programming Languages / General
• Table of Contents:
  1. Untyped Systems: Untyped Arithmetic Expressions, An ML Implementation of Arithmetic Expressions, The Untyped Lambda-Calculus, Nameless Representation of Terms, An ML Implementation of the Lambda-Calculus
  2. Simple Types: Typed Arithmetic Expressions, Simply Typed Lambda-Calculus, An ML Implementation of Simple Types, Simple Extensions, Normalization, References, Exceptions
  3. Subtyping: Subtyping, Metatheory of Subtyping, An ML IMplementation of Subtyping, Case Study: Imperative Objects, Case Study: Featherweight Java
  4. Recursive Types: Recursive Types, Metatheory of Recursive Types
  5. Polymorphism: Type Reconstruction, Universal Types, Existential Types, An ML Implementation of System F, Bounded Quantification, Case Study: Imperative Objects, Redux, Metatheory of Bounded Quantification
  6. Higher-Order Systems: Type Operators and Kinding, Higher-Order Polymorphism, Higher-Order Subtyping, Case Study: Purely Functional Objects

Practical Foundations for Programming Languages

• Author: Robert Harper / Cambridge University Press
• Category: Programming Languages / General, Operational Semantics
• Table of Contents:
  1. Judgments and Rules: Syntactic Objects, Inductive Definitions, Hypothetical and General Judgments
  2. Statics and Dynamics: Statics, Dynamics, Type Safety, Evaluation Dynamics
  3. Function Types: Function Definitions and Values, Goedel's T, Plotkin's PCF
  4. Finite Data Types: Product Types, Sum Types, Pattern Matching, Generic Programming
  5. Infinite Data Types: Inductive and Co-Inductive Types, Recursive Types
  6. Dynamic Types: The Untyped Lambda-Calculus, Dynamic Typing, Hybrid Typing
  7. Variable Types: Girard's System F, Abstract Types, Constructors and Kinds
  8. Subtyping: Subtyping, Singleton Kinds
  9. Classes and Methods: Dynamic Dispatch, Inheritance
  10. Exceptions and Continuations: Control Stacks, Exceptions, Continuations
  11. Types and Propositions: Constructive Logic, Classical Logic
  12. Symbols: Symbols, Fluid Binding, Dynamic Classification
  13. State: Modernized Algol, Assignable References
  14. Laziness: lazy Evaluation, Polarization
  15. Parallelism: Nested Parallelism, FUtures and Speculations
  16. Concurrency: Process Calculus, Concurrent Algol, Distributed Algol
  17. Modularity: Components and LInking, Type Abstractions and Type Classes, Hierarchy and Parameterization
  18. Equational Reasoning: Equational Reasoning for T, Equational Reasoning for PCF, Parametricity, Process Equivalence

Essentials of Programming Languages

• Author: Daniel P. Friedman and Mitchell Wand / The MIT Press
• Category: Programming Languages/ General
• Table of Contents:
  1. Inductive Sets of Data
  2. Data Abstraction
  3. Expressions
  4. State
  5. Continuation-Passing INterpreters
  6. Continuation-Passing Style
  7. Types
  8. Modules
  9. Objects and Classes

Programming Languages and Lambda Calculi

• Author: Matthias Felleisen and Matthew Flatt
• Category: Programming Languages / General
• Summer 2006 Revised Version; DRAFT: July 12, 2006. Seems to be replaced by the book Semantics Engineering with PLT Redex, Felleisen, Findler and Flatt / The MIT Press, 2009
• Table of Contents
  1. Models of Languages: Computing with Text, Consistency of Evaluation, The Lambda-Calculus
  2. Models of Realistic Languages: ISWIM, Standard Reduction, Machines, SECD, Tail Calls, and Safe for Space, Continuations, Errors and Exceptions, Imperative Assignment
  3. Models for Typed Languages: Types, Simply Typed ISWIM, Variations on Simply Typed ISWIM, Polymorphism, Type Inference, Recursive Types, Data Abstraction and Existential Types, Subtyping, Objects and Classes

Type Theory and Functional Programming

• Author: Simon Thompson / Addison-Wesley, 1991
• Category: Functional Programming / Types, Logic
• Out of print. The author has made it freely available online.
• Table of Contents:
  1. Introduction to Logic: Propositional Logic, Prediate Logic
  2. Functional Programming and Lambda-Calculi: Functional Programming, The untyped Lambda-calculus, Evaluation, COnvertibility, Expressiveness, Type Lambda-Calculus, Strong normalisation, Further type constructors: the product, Base Types: Natural Numbers, General Recursion, Evaluation Revisited
  3. Constructive Mathematics
  4. Introduction to Type Theory: Propositional Logic: an Informal View, Judgements, Proofs and Derivations, The Rules for Propositional Calculus, The Curry-Howard Isomorphism, Some examples, Quantifiers, Base Types, The natural numbers, Well-founded types -- trees, Equality, Convertibility
  5. Exploring Type Theory: Assumptions, Naming and abbreviations, Revising the rules, Derivability, Computation, TT^c_0: Normalisation and its corollaries, Equalities and Identities, Different Equalities, Universes, Well-founded types, Expresibility, The Curry-Howard Isomorphism?
  6. Applying Type Theory: Recursion, A Case Study -- Quicksort, Dependent types and quantifiers, A Case Study -- Vectors, Proof Extraction: Top-Down Proof, Program Development -- Polish National Flag, Program Transformation, Imperative Programming, Examples in the literature
  7. Augmenting Type Theory: Background, The subset type, Propositions not types, Are subsets necessary? Quotient or Congruence Types, Case Study -- The Real Numbers, Strengthened rules; polymorphism, Well-founded recursion, Well-founded recursion in type theory, Inductive types, Co-inductions, Partial Objects and Types
  8. Foundations: Proof Theory, Model Theory, A General Framework for Logics
  9. Conclusions

Domain-Theoretic Foundations of Functional Programming

• Author: Thomas Streicher / World Scientific Pub Co Inc
• Category: Programming Languages/ Denotational Semantics
• Table of Contents:

Introduction to Functional Programming using Haskell

• Author: Richard Bird / Prentice Hall
• Category: Functional Programming/ Haskell
• Table of Contents:
  1. Fundamental concepts
  2. Simple datatypes
  3. Numbers
  4. Lists
  5. Examples
  6. Trees
  7. Efficiency
  8. Abstract datatypes
  9. Infinite lists
  10. Monads
  11. Parsing
  12. An automatic calculator