# Deepak Kapur

According to our database

^{1}, Deepak Kapur## Timeline

#### Legend:

Book In proceedings Article PhD thesis Other## Links

#### Homepage:

#### On csauthors.net:

## Bibliography

2017

Comprehensive Gröbner basis theory for a parametric polynomial ideal and the associated completion algorithm.

J. Systems Science & Complexity, 2017

Preface - Special Issue of Selected Extended Papers of IJCAR 2014.

J. Autom. Reasoning, 2017

Connecting Program Synthesis and Reachability: Automatic Program Repair Using Test-Input Generation.

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2017

2016

Interpolation synthesis for quadratic polynomial inequalities and combination with \textit{EUF}.

CoRR, 2016

Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF.

Proceedings of the Automated Reasoning - 8th International Joint Conference, 2016

2015

Decoding femininity in computer science in India.

Commun. ACM, 2015

An Algorithm to Check Whether a Basis of a Parametric Polynomial System is a Comprehensive Gröbner Basis and the Associated Completion Algorithm.

Proceedings of the 2015 ACM on International Symposium on Symbolic and Algebraic Computation, 2015

Unification and Matching in Hierarchical Combinations of Syntactic Theories.

Proceedings of the Frontiers of Combining Systems - 10th International Symposium, 2015

When Is a Formula a Loop Invariant?

Proceedings of the Logic, Rewriting, and Concurrency, 2015

2014

DIG: A Dynamic Invariant Generator for Polynomial and Array Invariants.

ACM Trans. Softw. Eng. Methodol., 2014

An Abstract Domain to Infer Octagonal Constraints with Absolute Value.

Proceedings of the Static Analysis - 21st International Symposium, 2014

Using dynamic analysis to generate disjunctive invariants.

Proceedings of the 36th International Conference on Software Engineering, 2014

On Asymmetric Unification and the Combination Problem in Disjoint Theories.

Proceedings of the Foundations of Software Science and Computation Structures, 2014

2013

An efficient method for computing comprehensive Gröbner bases.

J. Symb. Comput., 2013

An efficient algorithm for computing a comprehensive Gröbner system of a parametric polynomial system.

J. Symb. Comput., 2013

On invariant checking.

J. Systems Science & Complexity, 2013

Synthesizing Switching Controllers for Hybrid Systems by Continuous Invariant Generation

CoRR, 2013

Hierarchical Combination of Unication Algorithms (Extended Abstract).

Proceedings of the 27th International Workshop on Unification, 2013

Hierarchical Combination.

Proceedings of the Automated Deduction - CADE-24, 2013

Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis.

Proceedings of the Automated Deduction - CADE-24, 2013

Synthesizing Switching Controllers for Hybrid Systems by Generating Invariants.

Proceedings of the Theories of Programming and Formal Methods, 2013

Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants.

Proceedings of the Automated Reasoning and Mathematics, 2013

Harald Ganzinger's Legacy: Contributions to Logics and Programming.

Proceedings of the Programming Logics - Essays in Memory of Harald Ganzinger, 2013

Elimination Techniques for Program Analysis.

Proceedings of the Programming Logics - Essays in Memory of Harald Ganzinger, 2013

2012

A brief introduction to Wen-Tsun Wu's academic career.

J. Symb. Comput., 2012

Preface.

J. Symb. Comput., 2012

A "Hybrid" Approach for Synthesizing Optimal Controllers of Hybrid Systems: A Case Study of the Oil Pump Industrial Example

CoRR, 2012

Termination Analysis of Imperative Programs Using Bitvector Arithmetic.

Proceedings of the Verified Software: Theories, Tools, Experiments, 2012

Program Analysis Using Quantifier-Elimination Heuristics - (Extended Abstract).

Proceedings of the Theory and Applications of Models of Computation, 2012

Using dynamic analysis to discover polynomial and array invariants.

Proceedings of the 34th International Conference on Software Engineering, 2012

A "Hybrid" Approach for Synthesizing Optimal Controllers of Hybrid Systems: A Case Study of the Oil Pump Industrial Example.

Proceedings of the FM 2012: Formal Methods, 2012

Effective Symbolic Protocol Analysis via Equational Irreducibility Conditions.

Proceedings of the Computer Security - ESORICS 2012, 2012

Rewriting Induction + Linear Arithmetic = Decision Procedure.

Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012

2011

Unification over Distributive Exponentiation (Sub)Theories.

Journal of Automata, Languages and Combinatorics, 2011

Termination Analysis of C Programs Using Compiler Intermediate Languages.

Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, 2011

Protocol analysis in Maude-NPA using unification modulo homomorphic encryption.

Proceedings of the 13th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2011

Computing comprehensive Gröbner systems and comprehensive Gröbner bases simultaneously.

Proceedings of the Symbolic and Algebraic Computation, International Symposium, 2011

2010

Unification modulo a partial theory of exponentiation

Proceedings of the Proceedings 24th International Workshop on Unification, 2010

Shape Analysis with Reference Set Relations.

Proceedings of the Verification, 2010

Idle Port Scanning and Non-interference Analysis of Network Protocol Stacks Using Model Checking.

Proceedings of the 19th USENIX Security Symposium, 2010

Coverset Induction with Partiality and Subsorts: A Powerlist Case Study.

Proceedings of the Interactive Theorem Proving, First International Conference, 2010

A new algorithm for computing comprehensive Gröbner systems.

Proceedings of the Symbolic and Algebraic Computation, International Symposium, 2010

Induction, Invariants, and Abstraction.

Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010

2009

An Algorithm for Computing a Gröbner Basis of a Polynomial Ideal over a Ring with Zero Divisors.

Mathematics in Computer Science, 2009

Cayley-Dixon projection operator for multi-univariate composed polynomials.

J. Symb. Comput., 2009

Operational Termination of Conditional Rewriting with Built-in Numbers and Semantic Data Structures.

Electr. Notes Theor. Comput. Sci., 2009

Termination of Context-Sensitive Rewriting with Built-In Numbers and Collection Data Structures.

Proceedings of the Functional and Constraint Logic Programming, 2009

Identification of logically related heap regions.

Proceedings of the 8th International Symposium on Memory Management, 2009

A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs.

Proceedings of the Automated Deduction, 2009

2008

Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures.

Proceedings of the Rewriting Techniques and Applications, 19th International Conference, 2008

Sharing analysis of arrays, collections, and recursive structures.

Proceedings of the 8th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, 2008

Identification of Heap-Carried Data Dependence Via Explicit Store Heap Models.

Proceedings of the Languages and Compilers for Parallel Computing, 2008

Efficient Context-Sensitive Shape Analysis with Graph Based Heap Models.

Proceedings of the Compiler Construction, 17th International Conference, 2008

Multivariate Resultants in Bernstein Basis.

Proceedings of the Automated Deduction in Geometry - 7th International Workshop, 2008

2007

Automatic generation of polynomial invariants of bounded degree using abstract interpretation.

Sci. Comput. Program., 2007

Generating all polynomial invariants in simple loops.

J. Symb. Comput., 2007

Heap analysis in the presence of collection libraries.

Proceedings of the 7th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, 2007

Dependency Pairs for Rewriting with Non-free Constructors.

Proceedings of the Automated Deduction, 2007

2006

Preface on the contributed papers.

J. Symb. Comput., 2006

Bruno Buchberger - A life devoted to symbolic computation.

J. Symb. Comput., 2006

A Quantifier-Elimination Based Heuristic for Automatically Generating Inductive Assertions for Programs.

J. Systems Science & Complexity, 2006

Third Special Issue on Techniques for Automated Termination Proofs.

J. Autom. Reasoning, 2006

Interpolation for data structures.

Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2006

Inductive Decidability Using Implicit Induction.

Proceedings of the Logic for Programming, 2006

A Static Heap Analysis for Shape and Connectivity: Unified Memory Analysis: The Base Framework.

Proceedings of the Languages and Compilers for Parallel Computing, 2006

Conditions for determinantal formula for resultant of a polynomial system.

Proceedings of the Symbolic and Algebraic Computation, International Symposium, 2006

2005

Preface.

J. Autom. Reasoning, 2005

Preface.

J. Autom. Reasoning, 2005

Towards Dynamic Partitioning of Reactive System Behavior: A Train Controller Case Study.

Proceedings of the Reliable Systems on Unreliable Networked Platforms, 2005

Automatically Generating Loop Invariants Using Quantifier Elimination.

Proceedings of the Deduction and Applications, 23.-28. October 2005, 2005

Cayley-Dixon Resultant Matrices of Multi-univariate Composed Polynomials.

Proceedings of the Computer Algebra in Scientific Computing, 8th International Workshop, 2005

A Unification Algorithm for Analysis of Protocols with Blinded Signatures.

Proceedings of the Mechanizing Mathematical Reasoning, 2005

2004

Resultants for unmixed bivariate polynomial systems produced using the Dixon formulation.

J. Symb. Comput., 2004

Constructing Sylvester-type resultant matrices using the Dixon formulation.

J. Symb. Comput., 2004

Preface.

J. Autom. Reasoning, 2004

Preface.

J. Autom. Reasoning, 2004

Preface.

J. Autom. Reasoning, 2004

An Abstract Interpretation Approach for Automatic Generation of Polynomial Invariants.

Proceedings of the Static Analysis, 11th International Symposium, 2004

Automatic generation of polynomial loop.

Proceedings of the Symbolic and Algebraic Computation, 2004

Support hull: relating the cayley-dixon resultant constructions to the support of a polynomial system.

Proceedings of the Symbolic and Algebraic Computation, 2004

Program Verification Using Automatic Generation of Invariants.

Proceedings of the Theoretical Aspects of Computing, 2004

2003

Exact resultants for corner-cut unmixed multivariate polynomial systems using the Dixon formulation.

J. Symb. Comput., 2003

Announcement.

J. Autom. Reasoning, 2003

On the relationship between the Dixon-based resultant construction and the supports of polynomial systems.

ACM SIGSAM Bulletin, 2003

Automatic Generation of Generalization Lemmas for Proving Properties of Tail-Recursive Definitions.

Proceedings of the Theorem Proving in Higher Order Logics, 16th International Conference, 2003

An E-unification Algorithm for Analyzing Protocols That Use Modular Exponentiation.

Proceedings of the Rewriting Techniques and Applications, 14th International Conference, 2003

Model Checking Reconfigurable Processor Configurations for Safety Properties.

Proceedings of the Field Programmable Logic and Application, 13th International Conference, 2003

Deciding Inductive Validity of Equations.

Proceedings of the Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28, 2003

Automatic Generation of Simple Lemmas from Recursive Definitions Using Decision Procedures - Preliminary Report.

Proceedings of the Advances in Computing Science, 2003

2002

On the efficiency and optimality of Dixon-based resultant methods.

Proceedings of the Symbolic and Algebraic Computation, 2002

A Rewrite Rule Based Framework for Combining Decision Procedures.

Proceedings of the Frontiers of Combining Systems, 4th International Workshop, 2002

2001

Designing a Controller for a Multi-Train Multi-Track System.

Electr. Notes Theor. Comput. Sci., 2001

Dependency Pairs for Equational Rewriting.

Proceedings of the Rewriting Techniques and Applications, 12th International Conference, 2001

A Survey: Applying Formal Methods to a Software Intensive System.

Proceedings of the 6th IEEE International Symposium on High-Assurance Systems Engineering (HASE 2001), 2001

Decidable Classes of Inductive Theorems.

Proceedings of the Automated Reasoning, First International Joint Conference, 2001

Rewriting, Induction and Decision Procedures: A Case Study of Presburger Arithmetic.

Proceedings of the Symbolic Algebraic Methods and Verification Methods, 2001

2000

Using an induction prover for verifying arithmetic circuits.

STTT, 2000

Conditions for exact resultants using the Dixon formulation.

Proceedings of the 2000 International Symposium on Symbolic and Algebraic Computation, 2000

Extending Decision Procedures with Induction Schemes.

Proceedings of the Automated Deduction, 2000

1998

Transformational Methodology for Proving Termination of Logic Programs.

J. Log. Program., 1998

Mechanical Verification of Adder Circuits using Rewrite Rule Laboratory.

Formal Methods in System Design, 1998

Geometric, Algebraic, and Thermophysical Techniques for Object Recognition in IR Imagery.

Computer Vision and Image Understanding, 1998

Proving Associative-Communicative Termination Using RPO-Compatible Orderings.

Proceedings of the Automated Deduction in Classical and Non-Classical Logics, 1998

IBDL: A Language for Interface Behavior Specification and Testing.

Proceedings of the 4th USENIX Conference on Object-Oriented Technologies and Systems (COOTS), 1998

Mechanizing Reasoning about Large Finite Tables in a Rewrite Based Theorem Prover.

Proceedings of the Advances in Computing Science, 1998

1997

Proving Termination of GHC Programs.

New Generation Comput., 1997

Rewriting, Decision Procedures and Lemma Speculation for Automated Hardware Verification.

Proceedings of the Theorem Proving in Higher Order Logics, 10th International Conference, 1997

A Total, Ground path Ordering for Proving Termination of AC-Rewrite Systems.

Proceedings of the Rewriting Techniques and Applications, 8th International Conference, 1997

Shostak's Congruence Closure as Completion.

Proceedings of the Rewriting Techniques and Applications, 8th International Conference, 1997

Extraneous Factors in the Dixon Resultant Formulation.

Proceedings of the 1997 International Symposium on Symbolic and Algebraic Computation, 1997

Synthesizing Controllers for Hybrid Systems.

Proceedings of the Hybrid and Real-Time Systems, 1997

Mechanizing Verification of Arithmetic Circuits: SRT Division.

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

1996

New Uses of Linear Arithmetic in Automated Theorem Proving by Induction.

J. Autom. Reasoning, 1996

Sparsity Considerations in Dixon Resultants.

Proceedings of the Twenty-Eighth Annual ACM Symposium on the Theory of Computing, 1996

Distributed Larch Prover (DLP): An Experiment in Parallelizing a Rewrite-Rule Based Prover.

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

Rewrite-Based Automated Reasoning: Challenges Ahead.

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

Automating Proofs of Integrity Constraints in Situation Calculus.

Proceedings of the Foundations of Intelligent Systems, 9th International Symposium, 1996

Parallel User Interfaces for Parallel Applications.

Proceedings of the 5th International Symposium on High Performance Distributed Computing (HPDC '96), 1996

Mechanically Verifying a Family of Multiplier Circuits.

Proceedings of the Computer Aided Verification, 8th International Conference, 1996

Lemma Discovery in Automated Induction.

Proceedings of the Automated Deduction - CADE-13, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30, 1996

Automating Induction over Mutually Recursive Functions.

Proceedings of the Algebraic Methodology and Software Technology, 1996

Automated Geometric Reasoning: Dixon Resultants, Gröbner Bases, and Characteristic Sets.

Proceedings of the Automated Deduction in Geometry, 1996

Using Elimination Methods to Compute Thermophysical Algebraic Invariants from Infrared Imagery.

Proceedings of the Thirteenth National Conference on Artificial Intelligence and Eighth Innovative Applications of Artificial Intelligence Conference, 1996

1995

A Path Ordering for Proving Termination of AC Rewrite Systems.

J. Autom. Reasoning, 1995

Comparison of Various Multivariate Resultant Formulations.

Proceedings of the 1995 International Symposium on Symbolic and Algebraic Computation, 1995

Maximal Extensions os Simplification Orderings.

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

Automated Reasoning About Parallel Algorithms Using Powerlists.

Proceedings of the Algebraic Methodology and Software Technology, 1995

1994

An Overview of the Tecton Proof System.

Theor. Comput. Sci., 1994

An Automated Tool for Analyzing Completeness of Equational Specifications.

Proceedings of the 1994 International Symposium on Software Testing and Analysis, 1994

Algebraic and Geometric Reasoning Using Dixon Resultants.

Proceedings of the International Symposium on Symbolic and Algebraic Computation, 1994

Using Linear Arithmetic Procedure for Generating Induction Schemes.

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

1993

Proving Termination of GHC Programs.

Proceedings of the Logic Programming, 1993

1992

Complexity of Unification Problems with Associative-Commutative Operators.

J. Autom. Reasoning, 1992

Double-exponential Complexity of Computing a Complete Set of AC-Unifiers

Proceedings of the Seventh Annual Symposium on Logic in Computer Science (LICS '92), 1992

The Tecton Proof System.

Proceedings of the Formal Methods in Databases and Software Engineering, 1992

Rewriting Concepts in the Study of Termination of Logic Programs.

Proceedings of the ALPUK92, Proceedings of the 4th UK Conference on Logic Programming, London, 30 March, 1992

1991

Semi-Unification.

Theor. Comput. Sci., 1991

Automating Inductionless Induction Using Test Sets.

J. Symb. Comput., 1991

Sufficient-Completeness, Ground-Reducibility and their Complexity.

Acta Inf., 1991

The Tecton Proof System.

Proceedings of the Rewriting Techniques and Applications, 4th International Conference, 1991

Modeling generic polyhedral objects with constraints.

Proceedings of the IEEE Computer Society Conference on Computer Vision and Pattern Recognition, 1991

A Transformational Methodology for Proving Termination of Logic Programs.

Proceedings of the Computer Science Logic, 5th Workshop, 1991

A Case Study of the Completion Procedure: Proving Ring Commutativity Problems.

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

1990

On Ground-Confluence of Term Rewriting Systems

Inf. Comput., May, 1990

Unnecessary Inferences in Associative-Commutative Completion Procedures.

Mathematical Systems Theory, 1990

Inference Rules and Proof Procedures for Inequations.

J. Log. Program., 1990

Refutational Proofs of Geometry Theorems via Characteristic Set Computation.

Proceedings of the International Symposium on Symbolic and Algebraic Computation, 1990

A New Method for Proving Termination of AC-Rewrite Systems.

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

1989

Consider Only General Superpositions in Completion Procedures.

Proceedings of the Rewriting Techniques and Applications, 3rd International Conference, 1989

An Overview of Rewrite Rule Laboratory (RRL).

Proceedings of the Rewriting Techniques and Applications, 3rd International Conference, 1989

1988

Computability and Implementability Issues in Abstract Data Types.

Sci. Comput. Program., 1988

Only Prime Superpositions Need be Considered in the Knuth-Bendix Completion Procedure.

J. Symb. Comput., 1988

Computing a Gröbner Basis of a Polynomial Ideal over a Euclidean Domain.

J. Symb. Comput., 1988

Proving Equivalence of Different Axiomatizations of Free Groups.

J. Autom. Reasoning, 1988

Opening the AC-Unification Race.

J. Autom. Reasoning, 1988

Wu's Method and its Application to Perspective Viewing.

Artif. Intell., 1988

Geometric Reasoning and Artificial Intelligence: Introduction to the Special Volume.

Artif. Intell., 1988

A Refutational Approach to Geometry Theorem Proving.

Artif. Intell., 1988

A Multi-Level Geometric Reasoning System for Vision.

Artif. Intell., 1988

Semi-Unification.

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

A Mechanizable Induction Principle for Equational Specifications.

Proceedings of the 9th International Conference on Automated Deduction, 1988

First-Order Theorem Proving Using Conditional Rewrite Rules.

Proceedings of the 9th International Conference on Automated Deduction, 1988

RRL: A Rewrite Rule Laboratory.

Proceedings of the 9th International Conference on Automated Deduction, 1988

GEOMETER: A Theorem Prover for Algebraic Geometry.

Proceedings of the 9th International Conference on Automated Deduction, 1988

1987

Complexity of Matching Problems.

J. Symb. Comput., 1987

Matching, unification and complexity.

ACM SIGSAM Bulletin, 1987

Proof by Consistency.

Artif. Intell., 1987

On Sufficient-Completeness and Related Properties of Term Rewriting Systems.

Acta Inf., 1987

Reasoning in Systems of Equations and Inequations.

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

1986

Using Gröbner Bases to Reason About Geometry Problems.

J. Symb. Comput., 1986

Inductive Reasoning with Incomplete Specifications (Preliminary Report)

Proceedings of the Symposium on Logic in Computer Science (LICS '86), 1986

Geometry theorem proving using Hilbert's Nullstellensatz.

Proceedings of the SYMSAC 1986, 1986

Complexity of Sufficient-Completeness.

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

RRL: A Rewrite Rule Laboratory.

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

Proof by Induction Using Test Sets.

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

NP-Completeness of the Set Unification and Matching Problems.

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

1985

The Church-Rosser Property and Special Thue Systems.

Theor. Comput. Sci., 1985

A Finite Thue System with Decidable Word Problem and without Equivalent Finite Canonical System.

Theor. Comput. Sci., 1985

An O(|T|3) Algorithm for Testing the Church-Rosser Property of Thue Systems.

Theor. Comput. Sci., 1985

The Knuth-Bendix Completion Procedure and Thue Systems.

SIAM J. Comput., 1985

Worst-Case Choice for the Stable Marriage Problem.

Inf. Process. Lett., 1985

A Rewrite Rule Based Approach for Synthesizing Abstract Data Types.

Proceedings of the Mathematical Foundations of Software Development, 1985

A Path Ordering for Proving Termination of Term Rewriting Systems.

Proceedings of the Mathematical Foundations of Software Development, 1985

An Ideal-Theoretic Approach to Work Problems and Unification Problems over Finitely Presented Commutative Algebras.

Proceedings of the Rewriting Techniques and Applications, First International Conference, 1985

Complexity of Matching Problems.

Proceedings of the Rewriting Techniques and Applications, First International Conference, 1985

An Equational Approach to Theorem Proving in First-Order Predicate Calculus.

Proceedings of the 9th International Joint Conference on Artificial Intelligence. Los Angeles, 1985

Reasoning about three dimensional space.

Proceedings of the 1985 IEEE International Conference on Robotics and Automation, 1985

1984

Algorithms for Computing Groebner Bases of Polynomial Ideals over Various Euclidean Rings.

Proceedings of the EUROSAM 84, 1984

A Natural Proof System Based on rewriting Techniques.

Proceedings of the 7th International Conference on Automated Deduction, 1984

1983

On Proving Uniform Termination and Restricted Termination of Rewriting Systems.

SIAM J. Comput., 1983

1982

Derived Pairs, Overlap Closures, and Rewrite Dominoes: New Tools for Analyzing Term rewriting Systems.

Proceedings of the Automata, 1982

Rewrite Rule Theory and Abstract Data Type Analysis.

Proceedings of the Computer Algebra, 1982

1981

Operators and algebraic structures.

Proceedings of the 1981 conference on Functional programming languages and computer architecture, 1981

Tecton: A Language for Manipulating Generic Objects.

Proceedings of the Program Specification, 1981

1980

Expressiveness of the Operation Set of a Data Abstraction.

Proceedings of the Conference Record of the Seventh Annual ACM Symposium on Principles of Programming Languages, 1980