| 1. |
- Barthes, Gilles, et al.
(författare)
-
Introduction to the Special Issue on Dependent Type Theory Meets Practical Programming
- 2004
-
Ingår i: Journal of Functional Programming. - 1469-7653 .- 0956-7968. ; 14:1, s. 1-2
-
Tidskriftsartikel (övrigt vetenskapligt/konstnärligt)abstract
- 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.
|
|
| 2. |
- Abel, Andreas, 1974, et al.
(författare)
-
Normalization by Evaluation for Martin-Löf Type Theory with Equality Judgements
- 2007
-
Ingår i: Proceedings of 22nd IEEE Annual Symposium on Logic in ComputerScience, Wroclaw, Poland, July 2007.. - : IEEE. - 1043-6871. - 0769529089 ; , s. 3-12
-
Tidskriftsartikel (refereegranskat)abstract
- The decidability of equality is proved for Martin-Löf type theory with a universe a la Russell and typed beta-eta-equality judgements. A corollary of this result is that the constructor for dependent function types is injective, a property which is crucial for establishing the correctness of the type-checking algorithm. The decision procedure uses normalization by evaluation, an algorithm which first interprets terms in a domain with untyped semantic elements and then extracts normal forms. The correctness of this algorithm is established using a PER-model and a logical relation between syntax and semantics.
|
|
| 3. |
- Abel, Andreas, 1974, et al.
(författare)
-
Normalization by evaluation for Martin-Löf type theory with one universe
- 2007
-
Ingår i: Mathematical Foundations of Programming Semantics, New Orleans, LA, USA, April 2007. Ed. M. Fiore. Electronic Notes in Theoretical Computer Science, Elsevier.. ; 173, s. 17-40
-
Konferensbidrag (refereegranskat)abstract
- We present an algorithm for computing normal terms and types in Martin-Löf type theory with one universe and eta-conversion. We prove that two terms or types are equal in the theory iff the normal forms are identical (as de Bruijn terms). It thus follows that our algorithm can be used for deciding equality in Martin-Löf type theory. The algorithm uses the technique of normalization by evaluation; normal forms are computed by first evaluating terms and types in a suitable model. The normal forms are then extracted from the semantic elements. We prove its completeness by a PER model and its soundness by a Kripke logical relation.
|
|
| 4. |
|
|
| 5. |
|
|
| 6. |
- Abel, Andreas, 1974, et al.
(författare)
-
Verifying a semantic βη-conversion test for martin-löf type theory
- 2008
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Berlin, Heidelberg : Springer Berlin Heidelberg. - 1611-3349 .- 0302-9743. - 9783540705932 ; 5133 LNCS, s. 29-56
-
Konferensbidrag (refereegranskat)abstract
- Type-checking algorithms for dependent type theories often rely on the interpretation of terms in some semantic domain of values when checking equalities. Here we analyze a version of Coquand's algorithm for checking the βη-equality of such semantic values in a theory with a predicative universe hierarchy and large elimination rules. Although this algorithm does not rely on normalization by evaluation explicitly, we show that similar ideas can be employed for its verification. In particular, our proof uses the new notions of contextual reification and strong semantic equality. The algorithm is part of a bi-directional type checking algorithm which checks whether a normal term has a certain semantic type, a technique used in the proof assistants Agda and Epigram. We work with an abstract notion of semantic domain in order to accommodate a variety of possible implementation techniques, such as normal forms, weak head normal forms, closures, and compiled code. Our aim is to get closer than previous work to verifying the type-checking algorithms which are actually used in practice.
|
|
| 7. |
|
|
| 8. |
-
Applied Semantics, International Summer School, APPSEM 2000, Caminha, Portugal, September 9-15, 2000, Advanced Lectures (LNCS 2395)
- 2002
-
Samlingsverk (redaktörskap) (refereegranskat)abstract
- This book presents revised and extended versions of lectures given at an international summer school on applied semantics that took place in Caminha, Portugal in September. The nine lectures included present recent developments in programming language research in a coherent and systematic way. Among the topics addressed are - description of existing programming languages features - design of new programming languages features - implementation and analysis of programming languages - transformation and generation of programs - verification of programs.
|
|
| 9. |
|
|
| 10. |
- Bezem, Marc, et al.
(författare)
-
On generalized algebraic theories and categories with families
- 2021
-
Ingår i: Mathematical Structures in Computer Science. - 0960-1295 .- 1469-8072. ; 31:9, s. 1006-1023
-
Tidskriftsartikel (refereegranskat)abstract
- We give a syntax independent formulation of finitely presented generalized algebraic theories as initial objects in categories of categories with families (cwfs) with extra structure. To this end, we simultaneously define the notion of a presentation sigma of a generalized algebraic theory and the associated category CwF(sigma) of small cwfs with a sigma-structure and cwf-morphisms that preserve sigma-structure on the nose. Our definition refers to the purely semantic notion of uniform family of contexts, types, and terms in CwF(sigma). Furthermore, we show how to syntactically construct an initial cwf with a sigma-structure. This result can be viewed as a generalization of Birkhoff's completeness theorem for equational logic. It is obtained by extending Castellan, Clairambault, and Dybjer's construction of an initial cwf. We provide examples of generalized algebraic theories for monoids, categories, categories with families, and categories with families with extra structure for some type formers of Martin-Lof type theory. The models of these are internal monoids, internal categories, and internal categories with families (with extra structure) in a small category with families. Finally, we show how to extend our definition to some generalized algebraic theories that are not finitely presented, such as the theory of contextual cwfs.
|
|
