Gérard P. Huet
According to our database1, Gérard P. Huet
Timeline
Legend:
Book In proceedings Article PhD thesis OtherLinks
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