Related papers: Syntax and Typing for Cedille Core

Cyp (Check Your Proofs) (Durner and Noschinski 2013; Traytel 2019) verifies proofs about Haskell-like programs. We extended Cyp with a pattern matcher for programs and proof terms, and a type checker. This allows to use Cyp for auto-grading…

This paper presents \tdl, a typed feature-based representation language and inference system. Type definitions in \tdl\ consist of type and feature constraints over the boolean connectives. \tdl\ supports open- and closed-world reasoning…

In the Calculus of Dependent Lambda Eliminations (CDLE), a pure Curry-style type theory, it is possible to generically {\lambda}-encode inductive datatypes which support course-of-values (CoV) induction. We present a datatype subsystem for…

In this tool demonstration, we give an overview of the Chameleon type debugger. The type debugger's primary use is to identify locations within a source program which are involved in a type error. By further examining these (potentially)…

As the name suggests, type-logical grammars are a grammar formalism based on logic and type theory. From the prespective of grammar design, type-logical grammars develop the syntactic and semantic aspects of linguistic phenomena…

We present Tores, a core language for encoding metatheoretic proofs. The novel features we introduce are well-founded Mendler-style (co)recursion over indexed data types and a form of recursion over objects in the index language to build…

Erlang is a functional programming language with dynamic typing. The language offers great flexibility for destructing values through pattern matching and dynamic type tests. Erlang also comes with a type language supporting parametric…

Type soundness is an important property of modern programming languages. In this paper we explore the idea that "well-typed languages are sound": the idea that the appropriate typing discipline over language specifications guarantees that…

We present a statically typed embedding of relational programming (specifically a dialect of miniKanren with disequality constraints) in Haskell. Apart from handling types, our dialect extends standard relational combinator repertoire with…

Cedille is a relatively recent tool based on a Curry-style pure type theory, without a primitive datatype system. Using novel techniques based on dependent intersection types, inductive datatypes with their induction principles are derived.…

Mella is a minimalistic dependently typed programming language and interactive theorem prover implemented in Haskell. Its main purpose is to investigate the effective integration of automated theorem provers in a pure and simple setting.…

Linear type theories, of various types and kinds, are of fundamental importance in most programming language research nowadays. In this paper we describe an extension of Benton's Linear-Non-Linear type theory and model for which we can…

Static verification of a program source code correctness is an important element of software reliability. Formal verification of software programs involves proving that a program satisfies a formal specification of its behavior. Many…

In this paper we describe how to leverage higher-order unification to type check a dependently typed language with meta-variables. The literature usually presents the unification algorithm as a standalone component, however the need to…

Proof assistants and programming languages based on type theories usually come in two flavours: one is based on the standard natural deduction presentation of type theory and involves eliminators, while the other provides a syntax in…

We present Turnstile+, a high-level, macros-based metaDSL for building dependently typed languages. With it, programmers may rapidly prototype and iterate on the design of new dependently typed features and extensions. Or they may create…

Coroutine, as a powerful programming construct, is widely used in asynchronous applications to replace thread-based programming or the callback hell. Using coroutines makes code more readable and maintainable, for its ability to transfer…

Bidirectional typing is a discipline in which the typing judgment is decomposed explicitly into inference and checking modes, allowing to control the flow of type information in typing rules and to specify algorithmically how they should be…

Dynamically typed programming languages are popular in education and the software industry. While presenting a low barrier to entry, they suffer from run-time type errors and longer-term problems in code quality and maintainability.…

We present a type theory combining both linearity and dependency by stratifying typing rules into a level for logics and a level for programs. The distinction between logics and programs decouples their semantics, allowing the type system…