Modern quantum programming languages integrate quantum resources and classical control. They must, on the one hand, be linearly typed to reflect the no-cloning property of quantum resources. On the other hand, high-level and practical languages should also support quantum circuits as first-class citizens, as well as families of circuits that are indexed by some classical parameters. Quantum programming languages thus need linear dependent type theory. This paper defines a general semantic structure for such a type theory via certain fibrations of monoidal categories. The categorical model of the quantum circuit description language Proto-Quipper-M by Rios and Selinger (2017) constitutes an example of such a fibration, which means that the language can readily be integrated with dependent types. We then devise both a general linear dependent type system and a dependently typed extension of Proto-Quipper-M, and provide them with operational semantics as well as a prototype implementation.
If code is law, then the language of law is a programming language. Lawyers and legal scholars can learn about law by studying programming-language theory, and programming-language tools can be usefully applied to legal problems. This article surveys the history of research on programming languages and law and presents ten promising avenues for future efforts. Its goals are to explain how the combination of programming languages and law is distinctive within the broader field of computer science and law, and to demonstrate with concrete examples the remarkable power of programming-language con…
Gate-based quantum programming languages are ubiquitous but measurement-based languages currently exist only on paper. This work introduces MCBeth, a quantum programming language which allows programmers to directly represent, program, and simulate measurement-based and cluster state computation by building upon the measurement calculus. While MCBeth programs are meant to be executed directly on hardware, to take advantage of current machines we also provide a compiler to gate-based instructions. We argue that there are clear advantages to measurement-based quantum computation compared to gate…
IBM Research（IBM研究公司/IBM研究（注：IBM Research通常译为IBM研究，属于企业研究机构，按要求提取到公司级别））
Deep probabilistic programming languages try to combine the advantages of deep learning with those of probabilistic programming languages. If successful, this would be a big step forward in machine learning and programming languages. Unfortunately, as of now, this new crop of languages is hard to use and understand. This paper addresses this problem directly by explaining deep probabilistic programming languages and indirectly by characterizing their current strengths and weaknesses.
Many quantum programs require circuits for addition, subtraction and logical operations. These circuits may be packaged within routines known as oracles. However, oracles can be tedious to code with current frameworks. To solve this problem the author developed Higher-Level Oracle Description Language (HODL) -- a C-style programming language for use on quantum computers -- to ease the creation of such circuits. The compiler translates high-level code written in HODL and converts it into OpenQASM, a gate-based quantum assembly language that runs on IBM Quantum Systems and compatible simulators.
Suenaga and Hasuo introduced a nonstandard programming language ${\bf While}^{\bf dt}$ which models hybrid systems. We demonstrate why ${\bf While}^{\bf dt}$ is not suitable for modeling actual computations.
We present a simple programming language based on Gödel numbering and prime factorization, enhanced with explicit, scoped loops, allowing for easy program composition. Further, we will present a theorem prover that allows expressing and working with formal systems. The theorem prover is simple as it relies merely on a substitution rule and set equality to derive theorems. Finally, we will represent the programming language in the theorem prover. We will show the syntax and semantics of both, and then provide a few example programs and their evaluation.
The $\mathitΠ$ family of reversible programming languages for boolean circuits is presented as a syntax of combinators witnessing type isomorphisms of algebraic datatypes. In this paper, we give a denotational semantics for this language, using the language of weak groupoids à la Homotopy Type Theory, and show how to derive an equational theory for it, presented by 2-combinators witnessing equivalences of reversible circuits. We establish a correspondence between the syntactic groupoid of the language and a formally presented univalent subuniverse of finite types. The correspondence relates 1-…
Many popular open source programming languages (Perl, Ruby or Python for example) have systems for distributing packaged source code that software developers can use when working in that particular programming language. This paper will consider the design principals that should be followed if designing such an open source code repository.
Context: Generic programming, as defined by Stepanov, is a methodology for writing efficient and reusable algorithms by considering only the required properties of their underlying data types and operations. Generic programming has proven to be an effective means of constructing libraries of reusable software components in languages that support it. Generics-related language design choices play a major role in how conducive generic programming is in practice. Inquiry: Several mainstream programming languages (e.g. Java and C++) were first created without generics; features to support generic p…
In this work we introduce Qumin, a novel quantum programming language with a focus on providing an easy to use, minimalist, high-level, and easily extensible platform for quantum programming. Qumin's design concentrates on encompassing the various interactions between classical and quantum computation via the use of two sublanguages: an untyped one that handles classical preparation and control, and one linearly typed that explicitly handles quantum routines. This allows the classical part of the language to be freely used for general programming while placing restrictions on the quantum part …
We propose a runtime architecture that can be used in the development of a quantum programming language and its programming environment. The proposed runtime architecture enables dynamic interaction between classical and quantum data following the restriction that a quantum computer is available in the cloud as a batch computer, with no interaction with the classical computer during its execution. It is done by leaving the quantum code generation for the runtime and introducing the concept of futures for quantum measurements. When implemented in a quantum programming language, those strategies…
Recently, user-centered methods have been proposed to improve the design of programming languages. In order to explore what benefits these methods might have for novice programming language designers, we taught a collection of user-centered programming language design methods to a group of eight students. We observed that natural programming and usability studies helped the students refine their language designs and identify opportunities for improvement, even in the short duration of a course project.
Comparing Selected Criteria of Programming Languages Java, PHP, C++, Perl, Haskell, AspectJ, Ruby, COBOL, Bash Scripts and Scheme Revision 1.0 - a Team CPLgroup COMP6411-S10 Term Report
Control Network Programming (CNP) is a programming paradigm which is being described with the maxim "Primitives + Control Network = Control Network program". It is a type of graphic programming. The Control Network is a recursive system of graphs; it can be a purely descriptive specification of the problem being solved. Clearly, "drawing" the control network does not include any programming. The Primitives are elementary, easily understandable and clearly specified actions. Ultimately, they have to be programmed. Historically, they are usually coded in Free Pascal. The actual code of the primi…
University of Edinburgh（爱丁堡大学）；The Alan Turing Institute（艾伦·图灵研究所）
We introduce a new application for inductive logic programming: learning the semantics of programming languages from example evaluations. In this short paper, we explored a simplified task in this domain using the Metagol meta-interpretive learning system. We highlighted the challenging aspects of this scenario, including abstracting over function symbols, nonterminating examples, and learning non-observed predicates, and proposed extensions to Metagol helpful for overcoming these challenges, which may prove useful in other domains.
This volume contains the post-proceedings of the 14th International Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL), held as a satellite workshop of ETAPS 2016 in Eindhoven, The Netherlands, on 2-3 April 2016.
GitHub is the most widely used social, distributed version control system. It has around 10 million registered users and hosts over 16 million public repositories. Its user base is also very active as GitHub ranks in the top 100 Alexa most popular websites. In this study, we collect GitHub's state in its entirety. Doing so, allows us to study new aspects of the ecosystem. Although GitHub is the home to millions of users and repositories, the analysis of users' activity time-series reveals that only around 10% of them can be considered active. The collected dataset allows us to investigate the …
Building on the observation that reverse-mode automatic differentiation (AD) -- a generalisation of backpropagation -- can naturally be expressed as pullbacks of differential 1-forms, we design a simple higher-order programming language with a first-class differential operator, and present a reduction strategy which exactly simulates reverse-mode AD. We justify our reduction strategy by interpreting our language in any differential $λ$-category that satisfies the Hahn-Banach Separation Theorem, and show that the reduction strategy precisely captures reverse-mode AD in a truly higher-order sett…
Jodhpur Institute of Engineering and Technology（焦特布尔工程技术学院）
This paper attempts to connects the evolution of computer languages with the evolution of life, where the later has been dictated by \emph{theory of evolution of species}, and tries to give supportive evidence that the new languages are more robust than the previous, carry-over the mixed features of older languages, such that strong features gets added into them and weak features of older languages gets removed. In addition, an analysis of most prominent programming languages is presented, emphasizing on how the features of existing languages have influenced the development of new programming …
This volume of the EPTCS contains the proceedings of the 15th international workshop on Qualitative Aspects of Programming Languages and Systems, QAPL 2017, held at April 23, 2017 in Uppsala, Sweden as a satellite event of ETAPS 2017, the 20th European Joint Conferencec on Theory and Practice of Software. The volume contains two invited contributions by Erika Abraham and by Andrea Vandin as well as six technical papers selected by the QAPL 2017 program committee.
The augmented version of C programming language is presented. The language was completed with a series of low-level and high-level facilities to enlarge the language usage spectrum to various computing systems, operations, users. The ambiguities and inconsistencies have been resolved by managing problematic and undefined languages elements through an interpretation and management similar to that used in the case of other C syntax based languages. The proposed augmentative completeness elements, through @C approach, preserve the spirit of C language and its basic characteristics through compati…
High-level reversible programming languages are few and far between and in general offer only rudimentary abstractions from the details of the underlying machine. Modern programming languages offer a wide array of language constructs and paradigms to facilitate the design of abstract interfaces, but we currently have a very limited understanding of the applicability of such features for reversible programming languages. We introduce the first reversible object-oriented programming language, ROOPL, with support for user-defined data types, class inheritance and subtype-polymorphism. The languag…
Programming language design requires making many usability-related design decisions. However, existing HCI methods can be impractical to apply to programming languages: they have high iteration costs, programmers require significant learning time, and user performance has high variance. To address these problems, we adapted both formative and summative HCI methods to make them more suitable for programming language design. We integrated these methods into a new process, PLIERS, for designing programming languages in a user-centered way. We evaluated PLIERS by using it to design two new program…
I present a new approach to teaching a graduate-level programming languages course focused on using systems programming ideas and languages like WebAssembly and Rust to motivate PL theory. Drawing on students' prior experience with low-level languages, the course shows how type systems and PL theory are used to avoid tricky real-world errors that students encounter in practice. I reflect on the curricular design and lessons learned from two years of teaching at Stanford, showing that integrating systems ideas can provide students a more grounded and enjoyable education in programming languages…
Interoperability is the ability of a programming language to work with systems based on different languages and paradigms. These days, many widely used high-level language impementations provide access to external functionalities. In this paper, we present some ideas on CLR interoperability focusing on the kind of constructs desirable by a programmer to this regard.
Current approaches to making programming languages and reasoning assistants more effective for people focus on leveraging feedback from users and on evaluating the success of particular techniques. These approaches, although helpful, may not result in systems that are as usable as possible, and may not lead to general design principles. This paper advocates for leveraging theories from cognitive science, focusing on cognitive load theory, to design more effective programming languages and reasoning assistants. Development of these theories may enable designers to create more effective programm…
In this chapter, we propose some future directions of work, potentially beneficial to Mathematics and its foundations, based on the recent import of methodology from the theory of programming languages into proof theory. This scientific essay, written for the audience of proof theorists as well as the working mathematician, is not a survey of the field, but rather a personal view of the author who hopes that it may inspire future and fellow researchers.
Ray, Devanbu and Filkov issued a rebuttal of our TOPLAS paper "On the Impact of Programming Languages on Code Quality: A Reproduction Study". Our paper reproduced "A Large-Scale Study of Programming Languages and Code Quality in GitHub", which appeared at FSE 2014 and was subsequently republished as a CACM research highlight in 2017. This article is a rebuttal to that rebuttal.
The increasingly concurrent and parallel landscape of hardware and software infrastructures demands the exploration and understanding of a wide variety of foundational and practical ideas. The International Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software (PLACES) is dedicated to work in this area. The workshop offers a forum for researchers from different fields to exchange new ideas about these challenges to modern and future programming, where concurrency and distribution are the norm rather than a marginal concern. The topic is central and combi…
