| a |
| alpha-equivalence | Critical Pair Analysis in Nominal Rewriting |
| arithmetization | From Tarski to Descartes: Formalization of the Arithmetization of Euclidean Geometry |
| automated reasoning | Determining automatically compass and straightedge unconstructibility in triangles |
| b |
| binding-time analysis | Automatic Staging via Partial Evaluation Techniques |
| bit-size | Bit-size reduction of triangular sets in two and three variables |
| c |
| Compass and straightedge construction | Determining automatically compass and straightedge unconstructibility in triangles |
| completeness | A rewrite-based computational model for functional logic programming |
| component-based software engineering | Expression Compatibility Problem |
| computational origami | A Mathematica module for Conformal Geometric Algebra and Origami Folding |
| confluence | Critical Pair Analysis in Nominal Rewriting |
| Conformal Geometric Algebra | A Mathematica module for Conformal Geometric Algebra and Origami Folding |
| congruence closure | A Data Structure to Handle Large Sets of Equal Terms |
| Coq | From Tarski to Descartes: Formalization of the Arithmetization of Euclidean Geometry
Verification of a brick Wang tiling algorithm
Towards Verified Construction for Planar Class of a Qualitative Spatial Representation |
| critical pairs | Critical Pair Analysis in Nominal Rewriting |
| cross-stage persistence | Automatic Staging via Partial Evaluation Techniques |
| d |
| data structure | A Data Structure to Handle Large Sets of Equal Terms |
| decision procedure | A Data Structure to Handle Large Sets of Equal Terms |
| delimited continuations | Implementing a stepper using delimited continuations |
| e |
| Expression Compatibility Problem | Expression Compatibility Problem |
| expression problem | Expression Compatibility Problem |
| expression simplification | A Data Structure to Handle Large Sets of Equal Terms |
| f |
| formal semantics | Expression Compatibility Problem |
| formalization | From Tarski to Descartes: Formalization of the Arithmetization of Euclidean Geometry |
| formalized mathematics | Compass-free Navigation of Mazes |
| functional logic programming | A rewrite-based computational model for functional logic programming |
| g |
| geometry | From Tarski to Descartes: Formalization of the Arithmetization of Euclidean Geometry
Compass-free Navigation of Mazes |
| i |
| interactive theorem proving | Compass-free Navigation of Mazes |
| l |
| Lagrange interpolation | Bit-size reduction of triangular sets in two and three variables |
| lexicographic Groebner bases | Bit-size reduction of triangular sets in two and three variables |
| Lightweight Family Polymorphism | Expression Compatibility Problem |
| m |
| Mathematica | A Mathematica module for Conformal Geometric Algebra and Origami Folding |
| multiplicity | Bit-size reduction of triangular sets in two and three variables |
| n |
| narrowing | A rewrite-based computational model for functional logic programming |
| network monitors | Space Analysis of a Predicate Logic Fragment for the Specification of Stream Monitors |
| Nominal rewriting | Critical Pair Analysis in Nominal Rewriting |
| p |
| partial evaluation | Automatic Staging via Partial Evaluation Techniques |
| planarity | Towards Verified Construction for Planar Class of a Qualitative Spatial Representation |
| PLCA | Towards Verified Construction for Planar Class of a Qualitative Spatial Representation |
| predicate logic | Space Analysis of a Predicate Logic Fragment for the Specification of Stream Monitors |
| program verification | Verification of a brick Wang tiling algorithm |
| proof assistant | Towards Verified Construction for Planar Class of a Qualitative Spatial Representation |
| q |
| qualitative spatial reasoning | Towards Verified Construction for Planar Class of a Qualitative Spatial Representation |
| s |
| shift and reset | Implementing a stepper using delimited continuations |
| soundness | A rewrite-based computational model for functional logic programming |
| space complexity | Space Analysis of a Predicate Logic Fragment for the Specification of Stream Monitors |
| staging | Automatic Staging via Partial Evaluation Techniques |
| stepper | Implementing a stepper using delimited continuations |
| strategies | A rewrite-based computational model for functional logic programming |
| symbolic computation | Determining automatically compass and straightedge unconstructibility in triangles |
| t |
| Tarski's system of geometry | From Tarski to Descartes: Formalization of the Arithmetization of Euclidean Geometry |
| term equivalence | A Data Structure to Handle Large Sets of Equal Terms |
| theory of equality | A Data Structure to Handle Large Sets of Equal Terms |
| Triangular Sets | Bit-size reduction of triangular sets in two and three variables |
| w |
| Wang tiling | Verification of a brick Wang tiling algorithm |
