# Gérard P. Huet

According to our database

^{1}, Gérard P. Huet## Timeline

#### Legend:

Book In proceedings Article PhD thesis Other## Links

#### Homepage:

#### On csauthors.net:

## Bibliography

2017

Computing with relational machines.

Mathematical Structures in Computer Science, 2017

2016

Design and analysis of a lean interface for Sanskrit corpus annotation.

J. Language Modelling, 2016

Teaching Foundations of Computation and Deduction Through Literate Functional Programming and Type Theory Formalization.

Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction, 2016

2014

30 years of research and development around Coq.

Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

Sanskrit Linguistics Web Services.

Proceedings of the COLING 2014, 2014

2012

A Distributed Platform for Sanskrit Processing.

Proceedings of the COLING 2012, 2012

2011

Preface.

Mathematical Structures in Computer Science, 2011

2008

Formal Structure of Sanskrit Text: Requirements Analysis for a Mechanical Sanskrit Processor.

Proceedings of the Sanskrit Computational Linguistics, 2008

2006

Shallow syntax analysis in Sanskrit guided by semantic nets constraints.

Proceedings of the International Workshop on Research Issues in Digital Libraries, 2006

The Reactive Engine for Modular Transducers.

Proceedings of the Algebra, Meaning, and Computation, 2006

2005

A functional toolkit for morphological and phonological processing, application to a Sanskrit tagger.

J. Funct. Program., 2005

2003

Special issue on 'Logical frameworks and metalanguages'.

J. Funct. Program., 2003

Zen and the Art of Symbolic Computing: Light and Fast Applicative Algorithms for Computational Linguistics.

Proceedings of the Practical Aspects of Declarative Languages, 5th International Symposium, 2003

Automata Mista.

Proceedings of the Verification: Theory and Practice, 2003

2002

Srl Yantra Geometry.

Theor. Comput. Sci., 2002

Higher Order Unification 30 Years Later.

Proceedings of the Theorem Proving in Higher Order Logics, 15th International Conference, 2002

2001

From an Informal Textual Lexicon to a Well-Structured Lexical Database: An Experiment in Data Reverse Engineering.

Proceedings of the Eighth Working Conference on Reverse Engineering, 2001

2000

Constructive category theory.

Proceedings of the Proof, Language, and Interaction, Essays in Honour of Robin Milner, 2000

1998

Regular Böhm trees.

Mathematical Structures in Computer Science, 1998

1997

The Zipper.

J. Funct. Program., 1997

Finite-State Transducers as Regular Böhm Trees.

Proceedings of the Theoretical Aspects of Computer Software, Third International Symposium, 1997

1996

Design Proof Assistant (Abstract).

Proceedings of the Rewriting Techniques and Applications, 7th International Conference, 1996

1994

Residual Theory in lambda-Calculus: A Formal Development.

J. Funct. Program., 1994

1993

An Analysis of Böhm's Theorem.

Theor. Comput. Sci., 1993

1992

The Gallina Specification language: A Case Study.

Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1992

1991

Computations in Orthogonal Rewriting Systems, II.

Proceedings of the Computational Logic - Essays in Honor of Alan Robinson, 1991

Computations in Orthogonal Rewriting Systems, I.

Proceedings of the Computational Logic - Essays in Honor of Alan Robinson, 1991

1990

Design Issues for a Computer-aided Environment for Constructive Mathematics (Abstract).

Proceedings of the Design and Implementation of Symbolic Computation Systems, 1990

1989

The Constructive Engine.

Proceedings of the A Perspective in Theoretical Computer Science, 1989

1988

The Calculus of Constructions

Inf. Comput., 1988

1987

Induction Principles Formalized in the Calculus of Constructions.

Proceedings of the TAPSOFT'87: Proceedings of the International Joint Conference on Theory and Practice of Software Development, 1987

The Calculus of Constructions: State of the Art.

Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1987

1986

Complete Sets of Unifiers and Matchers in Equational Theories.

Theor. Comput. Sci., 1986

Theorem Proving Systems of the Formel Project.

Proceedings of the 8th International Conference on Automated Deduction, Oxford, England, July 27, 1986

Mechanizing Constructive Proofs (Abstract).

Proceedings of the 8th International Conference on Automated Deduction, Oxford, England, July 27, 1986

1985

A Selected Bibliography on Constructive Mathematics, Intuitionistic Type Theory and Higher Order Deduction.

J. Symb. Comput., 1985

Concepts mathématiques et informatiques formalisés dans le calcul des constructions.

Proceedings of the Logic Colloquium '85, Orsay, France, 1985

Cartesian closed Categories and Lambda- calculus.

Proceedings of the Combinators and Functional Programming Languages, 1985

Constructions: A Higher Order Proof System for Mechanizing Mathematics.

Proceedings of the EUROCAL '85, 1985

Deduction and Computation.

Proceedings of the Fundamentals of Artificial Intelligence: An Advanced Course, 1985

1984

The future of symbolic computation: mathematics versus languages.

ACM SIGSAM Bulletin, 1984

1983

Complete Sets of Unifiers and Matchers in Equational Theories.

Proceedings of the CAAP'83, 1983

1982

Proofs by Induction in Equational Theories with Constructors.

J. Comput. Syst. Sci., 1982

In Defense of Programming Languages Design.

ECAI, 1982

1981

A Complete Proof of Correctness of the Knuth-Bendix Completion Algorithm.

J. Comput. Syst. Sci., 1981

1980

Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems: Abstract Properties and Applications to Term Rewriting Systems.

J. ACM, 1980

Proofs by Induction in Equational Theories with Constructors

Proceedings of the 21st Annual Symposium on Foundations of Computer Science, 1980

1978

An Algorithm to Generate the Basis of Solutions to Homogeneous Linear Diophantine Equations.

Inf. Process. Lett., 1978

Proving and Applying Program Transformations Expressed with Second-Order Patterns.

Acta Inf., 1978

1977

Artificial Intelligence in Western Europe.

Proceedings of the 5th International Joint Conference on Artificial Intelligence. Cambridge, 1977

Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems

Proceedings of the 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October, 1977

1975

A Unification Algorithm for Typed lambda-Calculus.

Theor. Comput. Sci., 1975

unification in typed lambda calculus.

Proceedings of the Lambda-Calculus and Computer Science Theory, 1975

1973

The Undecidability of Unification in Third Order Logic

Information and Control, April, 1973

A Mechanization of Type Theory.

Proceedings of the 3rd International Joint Conference on Artificial Intelligence. Standford, 1973