Idris (programming language)

Idris is a purely-functional programming language with dependent types, optional lazy evaluation, and features such as a totality checker. Idris may be used as a proof assistant, but is designed to be a general-purpose programming language similar to Haskell. The Idris type system is similar to Agda's, and proofs are similar to Coq's, including tactics (theorem proving functions/procedures) via elaborator reflection. Compared to Agda and Coq, Idris prioritizes management of side effects and support for embedded domain-specific languages. Idris compiles to C (relying on a custom copying garbage collector using Cheney's algorithm) and JavaScript (both browser- and Node.js-based). There are third-party code generators for other platforms, including Java virtual machine (JVM), Common Intermediate Language (CIL), and LLVM. Idris is named after a singing dragon from the 1970s UK children's television program Ivor the Engine. Idris combines a number of features from relatively mainstream functional programming languages with features borrowed from proof assistants. The syntax of Idris shows many similarities with that of Haskell. A hello world program in Idris might look like this: module Main main : IO () main = putStrLn "Hello, World!" The only differences between this program and its Haskell equivalent are the single (instead of double) colon in the type signature of the main function, and the omission of the word "where" in the module declaration. Idris supports inductively-defined data types and parametric polymorphism. Such types can be defined both in traditional Haskell 98-like syntax: data Tree a = Node (Tree a) (Tree a) | Leaf a or in the more general generalized algebraic data type (GADT)-like syntax: data Tree : Type -> Type where Node : Tree a -> Tree a -> Tree a Leaf : a -> Tree a With dependent types, it is possible for values to appear in the types; in effect, any value-level computation can be performed during type checking.

À propos de ce résultat

Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.

Publications associées (14)

Unités associées (2)

Concepts associés (16)

Cours associés (3)

Séances de cours associées (26)

CS-628: Interactive Theorem Proving CS

A hands-on introduction to interactive theorem proving, proofs as programs, dependent types, and to the Coq proof assistant. Come learn how to write bug-free code!

CS-320: Computer language processing

We teach the fundamental aspects of analyzing and interpreting computer languages, including the techniques to build compilers. You will build a working compiler from an elegant functional language in

CS-214: Software construction

Learn how to design and implement reliable, maintainable, and efficient software using a mix of programming skills (declarative style, higher-order functions, inductive types, parallelism) and fundam

Agda (programming language)

Agda is a dependently typed functional programming language originally developed by Ulf Norell at Chalmers University of Technology with implementation described in his PhD thesis. The original Agda system was developed at Chalmers by Catarina Coquand in 1999. The current version, originally known as Agda 2, is a full rewrite, which should be considered a new language that shares a name and tradition. Agda is also a proof assistant based on the propositions-as-types paradigm, but unlike Coq, has no separate tactics language, and proofs are written in a functional programming style.

Terminaison d'un algorithme

La terminaison est une propriété fondamentale des algorithmes. Elle stipule que les calculs décrits par l'algorithme s'arrêteront. En général cet arrêt doit avoir lieu quelles que soient les données initiales que l'on fournit à l'algorithme. Si l'on veut insister sur ce point on parle alors souvent de terminaison uniforme, mais le plus généralement « terminaison » couvre aussi bien l'arrêt sur une donnée que l'arrêt sur toutes les données et c'est le contexte qui décide.

Uniqueness type

In computing, a unique type guarantees that an object is used in a single-threaded way, with at most a single reference to it. If a value has a unique type, a function applied to it can be optimized to update the value in-place in the object code. Such in-place updates improve the efficiency of functional languages while maintaining referential transparency. Unique types can also be used to integrate functional and imperative programming. Uniqueness typing is best explained using an example.

LISA – A Modern Proof System

Viktor Kuncak, Simon Guilloud, Sankalp Gambhir

We present LISA, a proof system and proof assistant for constructing proofs in schematic first-order logic and axiomatic set theory. The logical kernel of the system is a proof checker for first-order logic with equality and schematic predicate and fun ...

2023

Article Structure and functionality of a multimeric human COQ7:COQ9 complex

Matteo Dal Peraro, Luciano Andres Abriata

Coenzyme Q (CoQ) is a redox-active lipid essential for core metabolic pathways and antioxidant defense. CoQ is synthesized upon the mitochondrial inner membrane by an ill-defined "complex Q" metabolon. Here, we present structure-function analyses of a lipi ...

CELL PRESS2022

Scaling Language Features for Program Verification

Georg Stefan Schmid

Formal verification of real-world software systems remains challenging for a number of reasons, including lack of automation, friction in specifying properties, and limited support for the diverse programming paradigms used in industry. In this thesis we m ...

EPFL2022

Sans titre

Coq: Vue d'ensemble

Présente Coq et se concentre sur la démonstration du théorème et du _comm étape par étape.

Sans titre CS-628: Interactive Theorem Proving CS