logo pages de liens

Votre portail e-Learning
ENSup. et Minist. EN
Séminaire MaMuX
Mathématiques, musique et relations avec d'autres disciplines


Langages Fonctionnels - Functional languages

Bas de page


<http://www.dcs.gla.ac.uk/fp/> <http://www.cs.chalmers.se/ComputingScience/Research/Functional/>
Central to the current work within the programming logic group is the idea of a logical framework for programming ; i.e. a unified theory of formal systems in which many different logics can be conveniently expressed. In particular, much of our work is based on Martin-Löf's theory of types, which provides such a framework.
University of Nottingham



Curry is a universal programming language aiming to amalgamate the most important declarative programming paradigms, namely functional programming and logic programming. Moreover, it also covers the most important operational principles developed in the area of integrated functional logic languages: "residuation" and "narrowing"
<http://www-i2.informatik.rwth-aachen.de/~hanus/curry/index.html> <http://www-i2.informatik.rwth-aachen.de/Forschung/FP/Haskell/> <http://www.erlang.org/>
is a robust, fully-featured, optimising compiler for Haskell 98, GHC compiles Haskell to either native code or C.
This binary distribution doesn't work on RedHat 6.0.
Haskell is a general purpose, purely functional programming language. Haskell compilers are freely available for almost any computer.
a Haskell interpreter and programming environment for developing cool Haskell programs. Sources and binaries are freely available by anonymous FTP and on the World-Wide Web. The release and supporting documents can be downloaded from the Hugs home page.
Hotter than Haskell
Cayenne is a simple(?) functional language with a powerful type system. The basic types are functions, products, and sums. Functions and products use dependent types to gain additional power.
is a system for incrementally developing proofs and programs. Agda is also a functional language with dependent types. This language is very similar to cayenne and agda is intended to be a (almost) full implementation of it in the future.
Alfa is a successor of the proof editor Alf with a graphical user interface.
ALF is a language which combines functional and logic programming techniques. The foundation of ALF is Horn clause logic with equality which consists of predicates and Horn clauses for logic programming, and functions and equations for functional programming. Since ALF is a genuine integration of both programming paradigms, any functional expression can be used in a goal literal and arbitrary predicates can occur in conditions of equations. The operational semantics of ALF is based on the resolution rule to solve literals and narrowing to evaluate functional expressions.
A proof-assistant is a computer program with which a user can construct completely formal mathematical proofs in some kind of logical system. In contrast to a theorem prover, a proof-assistant cannot find proofs on its own.
developed at Carnegie Mellon by the SCandAL project
<http://www.cs.cmu.edu/~scandal/nesl.html> <http://www.mozart-oz.org/>
University of St Andrews
CLEAN is a state-of-the-art, pure and lazy functional programming language specially designed to make the development of real world applications possible.
The United Functions and Objects project has developed a programming language which unites functional and Object Oriented Programming techniques.
he HOL system is a powerful and widely used computer program for constructing formal specifications and proofs in higher order logic. The system is used in both industry and academia to support formal reasoning in many different areas, including hardware design and verification, reasoning about security, proofs about real-time systems, semantics of hardware description languages, compiler verification, program correctness, modelling concurrency, and program refinement. HOL is also used as an open platform for general theorem-proving research.
a simulator for the parallel execution of Glasgow Parallel Haskell (GPH) programs. Haskell is a non-strict, purely-functional programming language. GPH extends Haskell with annotations for sequential (seq) and parallel (par) composition.
Cayenne is a simple(?) functional language with a powerful type system. The basic types are functions, products, and sums. Functions and products use dependent types to gain additional power.



This is the web site is dedicated to the preservation, promotion and development of the TRAC programming language.
Haskell is a general purpose, purely functional programming language. Haskell compilers are freely available for almost any computer.



Chalmers University of Technology
Computer Science Department, Yale University
Functional Programming Computer Music Jazz
<http://www.cs.yale.edu/~hudak-paul.html> <http://www.base.com/gordoni/> <http://research.microsoft.com/Users/simonpj/#aspects>



<ftp://ftp.dcs.glasgow.ac.uk/pub/haskell/gofer/> <http://www.haskell.org/hugs/>
GHC-Current is basically a recent snapshot of the source tree, guaranteed to be taken at a point when the sources build successfully (but don't necessarily work!).
<http://research.microsoft.com/users/t-simonm/ghc/download_ghc_current.html> <ftp://ftp.cs.chalmers.se/pub/haskell/chalmers/0.9999.3/>
For Cayenne to work you need hbc and lmlc which can be found at ftp.cs.chalmers.se/pub/haskell/chalmers



Klaus Havelund
The Java PathFinder, JPF, is a translator from Java to Promela, the programming language of the SPIN model checker. The purpose is to establish a framework for verification and debugging of Java programs using model checking. The system detects deadlocks and violations of assertions stated by the programmer.
A substantial companion to Java
Pizza is an extension of Java with three important new features. Parametric polymorphism. First-class functions. Class cases and pattern matching.
Pizza compiles programs to ordinary Java Byte Code, and interfaces with existing Java code, retaining the broad compatibility of Java.



Philip Wadler
Philip Wadler
<http://www.cs.bell-labs.com/~wadler/topics/linear-logic.html> <http://www.dcs.gla.ac.uk/fp/authors/Simon_Peyton_Jones/>
Jean-Louis Krivine



KIV is an interactive theorem prover with a user definable object logic.
John Hughes



Jean-Paul Baquiast et Christophe Jacquemin
Les automates intelligents robotique, vie artificielle, réalité virtuelle



The mission of the Sisal Language Project is to develop high-performance functional compilers and runtime systems to simplify the process of writing scientific programs on parallel supercomputers and to help programmers develop functional scientific applications.
<http://jarl.cs.uop.edu/cop/cs/faculty/joseph/SisalTutorial/> <http://www.cit.gu.edu.au/~arock/entre/entre.html>
Jean Goubault-Larrecq Le 02 août 1999
Jean Goubault-Larrecq



Alfa is a WYSIWYG proof editor. It allows you to, interactively and incrementally, define theories (axioms and inference rules), formulate theorems and construct proofs of the theorems. All steps in the proof construction are immediately checked by the system and no erroneous proofs can be constructed. The logical framework used is Agda
<http://www.cs.chalmers.se/~hallgren/Alfa/userguide.html> <http://haskell.org/bookshelf/>



Edited by Graham Hutton, University of Nottingham
<http://www.cs.nott.ac.uk/Department/Staff/gmh/faq.html> <http://www.cis.ohio-state.edu/hypertext/faq/usenet/func-lang-faq/faq.html>






<http://www-i2.informatik.rwth-aachen.de/~hanus/FLP/implementations.html> <http://compiler.kaist.ac.kr/~khchoi/fp.html> <http://www.studyweb.com/computers/program/functional.htm>
Here is a list of functional programs applied to real-world tasks. The main criterion for being real-world is that the program was written primarily to perform some task, not primarily to experiment with functional programming.
<http://www.cs.bell-labs.com/~wadler/realworld/index.html> <http://www.cs.cmu.edu/~mleone/language-research.html>

 haut de page

Advertising :   If you see a reference in one of the files that is not linked, and you know of a link address to the appropriate document, please send me mail, and I will include the link in the document. Thanks very much in advance.
Avertissement :    Le classement par catégories est approximatif. Certains liens se retrouvent dans des rubriques différentes et sur plusieurs pages. Les commentaires sont généralement des courts extraits des pages référencées. Il est possible que certains liens nécessitent une mise à jour.
Tous commentaires ou remarques sont les bienvenus, vous pouvez les adresser à :

Les mises à jour demandées sont réalisées dès que possible et, sauf si c'est nécessaire, aucun message de réponse n'est expédié. Merci de m'écrire.

Copyright © 1999-2012 Jean-Paul Davalan - Reproduction interdite.