Special issue on Dependent Type Theory Meets Programming Practice CALL FOR PAPERS

2001 ◽  
Vol 11 (4) ◽  
pp. 437-437
Author(s):  
Gilles Barthe ◽  
Peter Dybjer ◽  
Peter Thiemann

Modern programming languages rely on advanced type systems that detect errors at compile-time. While the benefits of type systems have long been recognized, there are some areas where the standard systems in programming languages are not expressive enough. Language designers usually trade expressiveness for decidability of the type system. Some interesting programs will always be rejected (despite their semantical soundness) or be assigned uninformative types.There are several remedies to this situation. Dependent type systems, which allow the formation of types that explicitly depend on other types or values, are one of the most promising approaches. These systems are well-investigated from a theoretical point of view by logicians and type theorists. For example, dependent types are used in proof assistants to implement various logics and there are sophisticated proof editors for developing programs in a dependently typed language.To the present day, the impact of these developments on practical programming has been small, partially because of the level of sophistication of these systems and of their type checkers. Only recently, there have been efforts to integrate dependent systems into intermediate languages in compilers and programming languages. Additional uses have been identified in high-profile applications such as mobile code security, where terms of a dependently typed lambda calculus to encode safety proofs.A special issue of the Journal of Functional Programming will be devoted to the interplay between dependent type theory and programming practice. We welcome technical contributions in the field, as well as position papers that:[bull ] make researchers in programming languages aware of new developments and research directions on the theory side;[bull ] point out to theorists practical uses of advanced type systems and urge them to address theoretical problems arising in emerging applications.Authors who are concerned about the appropriateness of a topic are welcome to contact the guest editors. Manuscripts should be unpublished works and not submitted elsewhere. Revised and enhanced versions of papers published in conference proceedings that have not appeared in archival journals are eligible for submission. All submissions will be reviewed according to the usual standards of scholarship and originality.Submissions should be sent to Gilles Barthe ([email protected]), with a copy to Nasreen Ahmad ([email protected]). Submitted articles should be sent in postscript format, preferably gzipped and uuencoded. In addition, please send, as plain text, title, abstract and contact information.The submission deadline is December 1st, 2001.

2004 ◽  
Vol 14 (1) ◽  
pp. 1-2
Author(s):  
GILLES BARTHE ◽  
PETER DYBJEN ◽  
PETER THIEMANN

Modern programming languages rely on advanced type systems that detect errors at compile-time. While the benefits of type systems have long been recognized, there are some areas where the standard systems in programming languages are not expressive enough. Language designers usually trade expressiveness for decidability of the type system. Some interesting programs will always be rejected (despite their semantical soundness) or be assigned uninformative types.


10.29007/322q ◽  
2018 ◽  
Author(s):  
Andreas Abel

Sized types are a modular and theoretically well-understood tool for checking termination of recursive and productivity of corecursive definitions. The essential idea is to track structural descent and guardedness in the type system to make termination checking robust and suitable for strong abstractions like higher-order functions and polymorphism.To study the application of sized types to proof assistants and programming languages based on dependent type theory, we have implemented a core language with explicit handling of sizes. New considerations were necessary to soundly integrate sized types with dependencies and pattern matching, which was made possible by modern concepts such as inaccessible patterns and parametric function spaces.


2009 ◽  
Vol 19 (5) ◽  
pp. 545-579 ◽  
Author(s):  
SHIN-CHENG MU ◽  
HSIANG-SHANG KO ◽  
PATRIK JANSSON

AbstractRelational program derivation is the technique of stepwise refining a relational specification to a program by algebraic rules. The program thus obtained is correct by construction. Meanwhile, dependent type theory is rich enough to express various correctness properties to be verified by the type checker. We have developed a library, AoPA (Algebra of Programming in Agda), to encode relational derivations in the dependently typed programming language Agda. A program is coupled with an algebraic derivation whose correctness is guaranteed by the type system. Two non-trivial examples are presented: an optimisation problem and a derivation of quicksort in which well-founded recursion is used to model terminating hylomorphisms in a language with inductive types.


2018 ◽  
Vol 29 (3) ◽  
pp. 465-510 ◽  
Author(s):  
RASMUS E. MØGELBERG ◽  
MARCO PAVIOTTI

Just like any other branch of mathematics, denotational semantics of programming languages should be formalised in type theory, but adapting traditional domain theoretic semantics, as originally formulated in classical set theory to type theory has proven challenging. This paper is part of a project on formulating denotational semantics in type theories with guarded recursion. This should have the benefit of not only giving simpler semantics and proofs of properties such as adequacy, but also hopefully in the future to scale to languages with advanced features, such as general references, outside the reach of traditional domain theoretic techniques.Working inGuarded Dependent Type Theory(GDTT), we develop denotational semantics for Fixed Point Calculus (FPC), the simply typed lambda calculus extended with recursive types, modelling the recursive types of FPC using the guarded recursive types ofGDTT. We prove soundness and computational adequacy of the model inGDTTusing a logical relation between syntax and semantics constructed also using guarded recursive types. The denotational semantics is intensional in the sense that it counts the number of unfold-fold reductions needed to compute the value of a term, but we construct a relation relating the denotations of extensionally equal terms, i.e., pairs of terms that compute the same value in a different number of steps. Finally, we show how the denotational semantics of terms can be executed inside type theory and prove that executing the denotation of a boolean term computes the same value as the operational semantics of FPC.


2003 ◽  
Vol 13 (2) ◽  
pp. 261-293 ◽  
Author(s):  
GILLES BARTHE ◽  
VENANZIO CAPRETTA ◽  
OLIVIER PONS

Formalising mathematics in dependent type theory often requires to represent sets as setoids, i.e. types with an explicit equality relation. This paper surveys some possible definitions of setoids and assesses their suitability as a basis for developing mathematics. According to whether the equality relation is required to be reflexive or not we have total or partial setoid, respectively. There is only one definition of total setoid, but four different definitions of partial setoid, depending on four different notions of setoid function. We prove that one approach to partial setoids in unsuitable, and that the other approaches can be divided in two classes of equivalence. One class contains definitions of partial setoids that are equivalent to total setoids; the other class contains an inherently different definition, that has been useful in the modeling of type systems. We also provide some elements of discussion on the merits of each approach from the viewpoint of formalizing mathematics. In particular, we exhibit a difficulty with the common definition of subsetoids in the partial setoid approach.


2014 ◽  
Vol 49 (1) ◽  
pp. 503-515 ◽  
Author(s):  
Robert Atkey ◽  
Neil Ghani ◽  
Patricia Johann

2019 ◽  
Vol 3 (ICFP) ◽  
pp. 1-29 ◽  
Author(s):  
Daniel Gratzer ◽  
Jonathan Sterling ◽  
Lars Birkedal

Author(s):  
Aleš Bizjak ◽  
Hans Bugge Grathwohl ◽  
Ranald Clouston ◽  
Rasmus E. Møgelberg ◽  
Lars Birkedal

Sign in / Sign up

Export Citation Format

Share Document